Frama-C Bug Tracking System - Frama-C
View Issue Details
0001038Frama-CPlug-in > wppublic2011-12-05 15:132013-04-19 11:05
Frama-C Nitrogen-20111001 
Frama-C Fluorine-20130401 
0001038: lemma tacitly ignored in absense of C code
When 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).
No tags attached.
c ftest.c (43) 2011-12-05 15:13
Issue History
2011-12-05 15:13JochenNew Issue
2011-12-05 15:13JochenStatusnew => assigned
2011-12-05 15:13JochenAssigned To => correnson
2011-12-05 15:13JochenFile Added: ftest.c
2013-03-09 23:44yakobowskiNote Added: 0003741
2013-03-09 23:44yakobowskiStatusassigned => resolved
2013-03-09 23:44yakobowskiResolutionopen => fixed
2013-04-19 11:05signolesFixed in Version => Frama-C Fluorine
2013-04-19 11:05signolesStatusresolved => closed

2013-03-09 23:44   
Got fixed at some point, probably thanks to Typed model.