Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002282Frama-CPlug-in > wppublic2017-02-16 14:072017-02-16 14:11
Assigned Tocorrenson 
PlatformSilicon-20161101OSxubuntuOS Version
Product VersionFrama-C 14-Silicon 
Target VersionFixed in Version 
Summary0002282: applicability of Coq proof script depends on order of include files
DescriptionWe run "frama-c -wp -wp-script wp0.script -wp-model Typed+ref -wp-prop HeapMaximum -wp-prover coq make_heap_cpp.c" on the attached files. In the current form, the Coq proof script "wp0.script" works fine and proved the lemma "HeapMaximum" from file "make_heap_cpp.c". However, when that lemma is moved after the "axiomatic Count", which is completely unrelated, the same command doesn't work any longer. Using "-wp-out" shows that both versions differ in the location where lemma "HeapBounds" is available in Coq; this make it necessary to change the names used in the proof. The problem originated from lemma "HeapMaximum" being used for the verification of two different function contracts. For software engineering reasons, the order of #include files was different (since different files were preferred to be included in the ".c", rather than already in the ".h" file). This resulted in "lemma HeapMaximum" appearing before and after an "axiomatic", making "wp0.script" work and not work, respectively.
TagsNo tags attached.
Attached Filesc file icon make_heap_cpp.c [^] (842 bytes) 2017-02-16 14:07 [Show Content]
? file icon wp0.script [^] (2,064 bytes) 2017-02-16 14:07

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2017-02-16 14:07 Jochen New Issue
2017-02-16 14:07 Jochen Status new => assigned
2017-02-16 14:07 Jochen Assigned To => correnson
2017-02-16 14:07 Jochen File Added: make_heap_cpp.c
2017-02-16 14:07 Jochen File Added: wp0.script

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker