Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002336Frama-CPlug-in > wppublic2017-12-08 12:522017-12-08 12:54
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeveritytweakReproducibilityalways
StatusassignedResolutionopen 
PlatformSulfur-20171101OSOS VersionUbuntu 17.04
Product Version 
Target VersionFixed in Version 
Summary0002336: suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"
DescriptionRunning "frama-c -wp -wp-rte foo.c -wp-out wp-out" on the attached file fails to prove clauses "E1" (as expected) and "E2". The latter is provable from "E1" by axiom "a2". A look at file "main_post_E2_Alt-Ergo.mlw" reveals that "E1" isn't given as hypothesis, and hence axiom "a2" can't be applied. I cannot judge whether there is good reason for this behavior of Frama-C/Wp. If there isn't, I suggest that "E1" should be given as hypothesis to the proof obligation for "E2", similar to Frama-C/Wp's behavior on consecutive "assigns" clauses. The same applies to statement contracts.
TagsNo tags attached.
Attached Filesc file icon foo.c [^] (247 bytes) 2017-12-08 12:52 [Show Content]

- Relationships

-  Notes
(0006481)
Jochen (reporter)
2017-12-08 12:54

In fact, I observed the problem when I tried to prove an "ensures" from a statement contract, and inserted an easier-to-prove clause as another "ensures" before it. The suggested change would make this method work.

- Issue History
Date Modified Username Field Change
2017-12-08 12:52 Jochen New Issue
2017-12-08 12:52 Jochen Status new => assigned
2017-12-08 12:52 Jochen Assigned To => correnson
2017-12-08 12:52 Jochen File Added: foo.c
2017-12-08 12:54 Jochen Note Added: 0006481


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker