Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
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

- Relationships

-  Notes
(0003252)
correnson (manager)
2012-07-06 15:18

Fixed for Typed model (other models will be deprecated soon).

- Issue History
Date Modified Username Field Change
2011-07-28 08:29 patrick New Issue
2011-07-28 08:29 patrick Status new => assigned
2011-07-28 08:29 patrick Assigned To => correnson
2012-07-06 15:18 correnson Note Added: 0003252
2012-07-06 15:18 correnson Status assigned => resolved
2012-07-06 15:18 correnson Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker