search

marek-trtik / cbmc

C Bounded Model Checker
http://www.cprover.org/cbmc
Other
0 stars 0 forks source link

ldv_assert failure #18

Closed marek-trtik closed 6 years ago

marek-trtik commented 7 years ago

Fix the issue in:

https://sv-comp.sosy-lab.org/2018/results/results-verified/cbmc.2017-11-20_0143.results.sv-comp18.ConcurrencySafety-Main.xml.bz2.merged.xml.bz2.table.html

marek-trtik commented 6 years ago

It turns out that commenting the line: https://github.com/marek-trtik/cbmc/blob/sv-comp-2018-patches/src/ansi-c/library/pthread_lib.c#L330 fixes the problem. The cause, why the condition can be true in the benchmark is unknown.

marek-trtik commented 6 years ago

The hot-fix (fake-fix) is done in this commit: https://github.com/marek-trtik/cbmc/commit/2f91901d5527c18b5042a45dbc7a0f6e9d2404df