Skip to content

Unsoundness with context-insensitive analyses: sv-comp tests "list_search" #1302

@SchiJoha

Description

@SchiJoha

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.

auswertung

Metadata

Metadata

Assignees

Labels

bugrelationalRelational analyses (Apron, affeq, lin2var)unsound

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions