search

marek-trtik / cbmc

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

CBMC incorrectly provides false(unreach-call) in memleaks_test3_false-valid-free.i #12

Closed lucasccordeiro closed 7 years ago

lucasccordeiro commented 7 years ago

If we run CBMC as:

$cbmc memleaks_test3_false-valid-free.i --stop-on-fail

It correctly identifies the bug:

Violated property:
  file memleaks_test3_false-valid-free.i line 1440 function entry_point
  free argument must be dynamic object
  (void *)p == NULL || DYNAMIC_OBJECT((void *)p)

VERIFICATION FAILED

However, our script provides:

false(unreach-call)

It suggested that there is some bug in our script that parses the CBMC output.

marek-trtik commented 7 years ago

xtest.zip

lucasccordeiro commented 7 years ago

This has been fixed via commit 551280c3bf5bb325b51e08c633d37430964cf240.

Now, we correctly report FALSE(valid-free) as follows:

Violated property: file /Users/lucasccordeiro/sv-benchmarks/c/ldv-memsafety/memleaks_test3_false-valid-free.i line 1440 function entry_point free argument must be dynamic object (void )p == NULL || DYNAMIC_OBJECT((void )p)

VERIFICATION FAILED EC=10 FALSE(valid-free)