-
Notifications
You must be signed in to change notification settings - Fork 87
Unsoundness with context-insensitive analyses: sv-comp tests "list_search" #1302
Description
If all analyses are context insensitive, the sv-comp testcases list-properties/list_search-1.i and list-properties/list_search-2.i fail with the svcomp24.json configuration. (Similar to issue #1298)
During execution the error: [Error][Analyzer][Unsound] Both branches dead is thrown. This comes from the fact, that any traversal through the list is detected to be infinite. Hence the whole remaining code is declared dead.
To set all analyses context insensitive I changed the mCP.ml file in line 83 from cont_inse := map' find_id @@ get_string_list "ana.ctx_insens"; to cont_inse := xs;.
After compiling and executing the sv-comp testcase, Goblint incorrectly reports valid memory cleanup. The SV-COMP result is true, but false is expected.
I used those commands to run the testcases:
list_search-1:
./goblint --conf conf/svcomp24.json --sets ana.specification "CHECK( init(main()), LTL(G valid-memcleanup) )" ../../sv-benchmarks/c/list-properties/list_search-1.i
list_search-2:
./goblint --conf conf/svcomp24.json --sets ana.specification "CHECK( init(main()), LTL(G valid-memcleanup) )" ../../sv-benchmarks/c/list-properties/list_search-2.i
If only one of the analyses base, mallocWrapper, var_eq, apron, memLeak is analyzed context sensitively (and the remaining context insensitively), both tests produce the correct result (so the SV-COMP result is unknown). An overview can be found in the following picture.
