Frama-C Bug Tracking System - Frama-C
View Issue Details
0002226Frama-CKernelpublic2016-05-02 17:592016-05-04 13:43
0002226: insertion of "assert true" after a statement influences provability of the statement's contract
Running "frama-c -wp p1on.c" on the attached program proves both the statement contract in line 9 and the trivial assertion in line 11, as expected. However, if line 11 is commented out, Alt-Ergo immediately reports "unknown" on line 9. (Cvc4 runs into its timeout then.) The file "foo_stmt_post_Alt-Ergo.mlw" contains the goal "goal foo_stmt_post: false" for some reason. It seems that the statement contract is translated in a wrong way, unless the final trivla assertion is present in line 11.
No tags attached.
c p1on.c (108) 2016-05-02 17:59
Issue History
2016-05-02 17:59JochenNew Issue
2016-05-02 17:59JochenFile Added: p1on.c
2016-05-03 09:16JochenNote Added: 0006184
2016-05-03 11:10yakobowskiAssigned To => correnson
2016-05-03 11:10yakobowskiStatusnew => assigned
2016-05-03 11:37jensNote Added: 0006186
2016-05-04 13:40corrensonNote Added: 0006187
2016-05-04 13:43corrensonNote Edited: 0006187View Revisions

2016-05-03 09:16   
As far as I remember from yesterday, deleting the "if" statement caused the problem to disappear, and transforming it into a semantical equivalent form without "return", i.e. into "if (...) { ... b=3; ... }", also caused the problem to disappear. However, I can't validate my memories from this computer.
2016-05-03 11:37   
The problem also occurs under magnesium (the current version of Frama-C) running on top of OS X.
2016-05-04 13:40   
(edited on: 2016-05-04 13:43)
Yes this actually a problem of CFG computation inside WP. Putting (at least) an empty statement after a block-contract shall solves the problem.