goblint
Unsound no-overflow result in SV-COMP test with `bsearch`
For the sv-comp test termination-crafted/Binary_Search-1.c in the category no-overflow Goblint returns a wrong result.
The problem is that it has a function bsearch, which also exists in includes/stdlib.c
If I delete the function in stlib.c, the result changes to unknown.
The command: ./goblint --conf conf/svcomp22.json --set ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-crafted/Binary_Search-1.c results in the console output:
SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (includes/sv-comp.c:18:40-18:50)
[Error][Imprecise][Unsound] Function definition missing for bsearch (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-crafted/Binary_Search-1.c:21:3-21:16)
[Info][Imprecise] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-crafted/Binary_Search-1.c:21:3-21:16)
[Info][Imprecise] Invalidating expressions: Lval(Var(x, NoOffset)), Lval(Var(y, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-crafted/Binary_Search-1.c:21:3-21:16)
[Warning][Deadcode] Function "__VERIFIER_error" will never be called: 1LoC (includes/sv-comp.c:2:1-2:36)
[Warning][Deadcode] Function "__VERIFIER_assume" will never be called: 1LoC (includes/sv-comp.c:9:1-9:89)
[Warning][Deadcode] Function "__VERIFIER_nondet_bool" will never be called: 1LoC (includes/sv-comp.c:15:1-15:57)
[Warning][Deadcode] Function "__VERIFIER_nondet_char" will never be called: 1LoC (includes/sv-comp.c:16:1-16:55)
[Warning][Deadcode] Function "__VERIFIER_nondet_float" will never be called: 1LoC (includes/sv-comp.c:19:1-19:58)
[Warning][Deadcode] Function "__VERIFIER_nondet_double" will never be called: 1LoC (includes/sv-comp.c:20:1-20:61)
[Warning][Deadcode] Function "__VERIFIER_nondet_long" will never be called: 1LoC (includes/sv-comp.c:22:1-22:55)
[Warning][Deadcode] Function "__VERIFIER_nondet_pchar" will never be called: 1LoC (includes/sv-comp.c:23:1-23:58)
[Warning][Deadcode] Function "__VERIFIER_nondet_short" will never be called: 1LoC (includes/sv-comp.c:26:1-26:58)
[Warning][Deadcode] Function "__VERIFIER_nondet_uchar" will never be called: 1LoC (includes/sv-comp.c:29:1-29:74)
[Warning][Deadcode] Function "__VERIFIER_nondet_uint" will never be called: 1LoC (includes/sv-comp.c:30:1-30:71)
[Warning][Deadcode] Function "__VERIFIER_nondet_ulong" will never be called: 1LoC (includes/sv-comp.c:31:1-31:74)
[Warning][Deadcode] Function "__VERIFIER_nondet_unsigned" will never be called: 1LoC (includes/sv-comp.c:32:1-32:67)
[Warning][Deadcode] Function "__VERIFIER_nondet_ushort" will never be called: 1LoC (includes/sv-comp.c:33:1-33:77)
[Warning][Deadcode] Function "__VERIFIER_nondet_pointer" will never be called: 1LoC (includes/sv-comp.c:35:1-35:60)
SV-COMP result: true
[Error][Imprecise][Unsound] Function definition missing for bsearch (initfun:0:0)
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-crafted/Binary_Search-1.c:8: Warning: Incompatible declaration for bsearch (from .goblint/preprocessed/Binary_Search-1.i(3)).
Previous was at includes/stdlib.c:37 (from .goblint/preprocessed/stdlib.i (1)) (different type constructors: void * vs. int )
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-crafted/Binary_Search-1.c:8: Warning: def'n of func bsearch at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-crafted/Binary_Search-1.c:8 (sum 49803) conflicts with the one at includes/stdlib.c:38 (sum 1086600); keeping the one at includes/stdlib.c:38.
The fact that an SV-COMP program redefines a standard function is arguably not allowed and I've proposed to have it changed, including this benchmark: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1358. Although I think we didn't have a problem with this in SV-COMP 2022.
Oddly though, that output contains INVALIDATING ALL GLOBALS! as if we didn't find either copy of the function. I'm not sure what that's about.
The sv-benchmarks MR has been merged and this is no longer unsound in the preruns.