2021-03-03 02:40 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001038Frama-CPlug-in > wppublic2013-04-19 11:05
Assigned Tocorrenson 
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 Files
  • c file icon ftest.c (43 bytes) 2011-12-05 15:13 -
    //@ lemma l: \false;
    //void ftest(void) {}
    c file icon ftest.c (43 bytes) 2011-12-05 15:13 +




yakobowski (manager)

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
+Issue History