Fix incorrect results in ReachSafety-Heap
hbgit opened this issue · 0 comments
hbgit commented
Verification results from SV-COMP
-
../../sv-benchmarks/c/ldv-regression/sizeofparameters_test.i
Incorrect long int a = __VERIFIER_nondet_long(); representation
-
../../sv-benchmarks/c/ldv-regression/test27-2.c
Expected FALSE, but the result is TRUE
Check:
libfuzzer -> ERROR: UndefinedBehaviorSanitizer: SEGV on unknown address
KLEE -> memory error: out of bound pointer
OR -> Struct modeling error -
../../sv-benchmarks/c/ldv-regression/test28-1.c
>> Same ERROR as the ldv-regression/test27-2.c