Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001038Frama-CPlug-in > wppublic2011-12-05 15:132013-04-19 11:05
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeveritytextReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001038: lemma tacitly ignored in absense of C code
DescriptionWhen running "frama-c -wp -cpp-command 'gcc -C -E -I.' -pp-annot -wp-rte -wp-proof simplify -no-unicode -wp-warnings -wp-out ./out ftest.c" on the attached program, I don't get any warning that no proof obligation is generated for lemma "l".

Such a warning is printed, however, when some C code is added (e.g. uncomment the trivial function definition in line 2 to demonstrate).
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (43 bytes) 2011-12-05 15:13 [Show Content]

- Relationships

-  Notes
(0003741)
yakobowski (manager)
2013-03-09 23:44

Got fixed at some point, probably thanks to Typed model.

- Issue History
Date Modified Username Field Change
2011-12-05 15:13 Jochen New Issue
2011-12-05 15:13 Jochen Status new => assigned
2011-12-05 15:13 Jochen Assigned To => correnson
2011-12-05 15:13 Jochen File Added: ftest.c
2013-03-09 23:44 yakobowski Note Added: 0003741
2013-03-09 23:44 yakobowski Status assigned => resolved
2013-03-09 23:44 yakobowski Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker