Opened 5 days ago

#19 assigned defect

SYM: Spurious errors due to infeasible explicit values

Reported by: Vladimír Štill Owned by: Henrich Lauko
Priority: major Milestone: future
Component: LART Keywords:
Cc:

Description

It is possible to create programs manifesting not only division by 0, but also memory and control errors which are spurious and due to invalid explicit value in symbolic computations.

undef:

#include <assert.h>

int __VERIFIER_nondet_int();

int main() {
    int array[2];
    int x = __VERIFIER_nondet_int();
    array[1] = 42;
    if ( x == 1 )
        assert( array[x] == 42 );
    return 0;
}


error trace: |
  ASSUME (= var_0 #x00000001)
  FAULT:  conditional jump depends on an undefined value
  [0] FATAL: control error in userspace

memory:

#include <assert.h>

int __VERIFIER_nondet_int();

int main() {
    int array[2];
    int x = __VERIFIER_nondet_int();
    array[1] = 42;
    if ( x == 1 )
        assert( array[2 - x] == 42 );
    return 0;
}



error trace: |
  ASSUME (= var_0 #x00000001)
  FAULT: access of size 4 at [heap* 44646cae 8 ddp] is 4 bytes out of bounds
  [0] FATAL: memory error in userspace

division by 0:

#include <assert.h>

int __VERIFIER_nondet_int();

int main() {
    int array[2];
    int x = __VERIFIER_nondet_int();
    if ( x == 1 )
        assert( 42 / x == 42 );
    return 0;
}



error trace: |
  ASSUME (= var_0 #x00000001)
  FAULT: division by [i32 0 dt]
  [0] FATAL: integer arithmetic error in userspace

All of these programs are OK for CBMC.

There is also a patch in ~xstill/DIVINE/svc-2019 which adds these tests.

Change History (0)

Note: See TracTickets for help on using tickets.