SYM: Spurious errors due to infeasible explicit values

[Vladimír Štill]

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.

[mornfall]

Milestone renamed