hbgit/Map2Check

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