Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002226Frama-CKernelpublic2016-05-02 17:592016-05-04 13:43
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformSodium-20150201OSxubuntu14.04OS Version
Product Version 
Target VersionFixed in Version 
Summary0002226: insertion of "assert true" after a statement influences provability of the statement's contract
DescriptionRunning "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.
TagsNo tags attached.
Attached Filesc file icon p1on.c [^] (108 bytes) 2016-05-02 17:59 [Show Content]

- Relationships

-  Notes
(0006184)
Jochen (reporter)
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.
(0006186)
jens (reporter)
2016-05-03 11:37

The problem also occurs under magnesium (the current version of Frama-C) running on top of OS X.
(0006187)
correnson (manager)
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.


- Issue History
Date Modified Username Field Change
2016-05-02 17:59 Jochen New Issue
2016-05-02 17:59 Jochen File Added: p1on.c
2016-05-03 09:16 Jochen Note Added: 0006184
2016-05-03 11:10 yakobowski Assigned To => correnson
2016-05-03 11:10 yakobowski Status new => assigned
2016-05-03 11:37 jens Note Added: 0006186
2016-05-04 13:40 correnson Note Added: 0006187
2016-05-04 13:43 correnson Note Edited: 0006187 View Revisions


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker