Frama-C Bug Tracking System - Frama-C
View Issue Details
0000895Frama-CPlug-in > wppublic2011-07-28 08:292012-09-19 17:16
Reporterpatrick 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0000895: Proof obligations of lemma properties
DescriptionProof obligations of lemma properties are not generated.

Revision: 14360
Additional Informationcat test_po_lemma1.c
//@ lemma l: 2 == 1 + 1 ;
//@ ensures p: \true ;
void f (void) {
  return ;
}

> frama-c -wp -wp-model Store test_po_lemma1.c -wp-warnings
test_po_lemma1.c:1:[wp] warning: Proof obligation for property 'l' not generated.
TagsNo tags attached.
Attached Files

Notes
(0003252)
correnson   
2012-07-06 15:18   
Fixed for Typed model (other models will be deprecated soon).

Issue History
2011-07-28 08:29patrickNew Issue
2011-07-28 08:29patrickStatusnew => assigned
2011-07-28 08:29patrickAssigned To => correnson
2012-07-06 15:18corrensonNote Added: 0003252
2012-07-06 15:18corrensonStatusassigned => resolved
2012-07-06 15:18corrensonResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed