Frama-C Bug Tracking System - Frama-C
View Issue Details
0000877Frama-CPlug-in > RTEpublic2011-07-06 10:102012-05-16 18:22
yakobowski 
pherrmann 
normalmajoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Nitrogen-20111001 
0000877: RTE does not generate assertions for non initialized arguments
Calling the WP (or Jessie for that matter) on the following code results in all goals being proven. Yet, there is a RTE on the call to max, because a is not initialized. I tend to think that -rte-precond should add \initialized(a) and \initialized(b) to the local contract for the call to max, but there is perhaps another better way. Anyway, either RTE or the WP are faulty here. /*@ ensures \result == (a < b ? a : b); */ int max(int a, int b) { return (a < b ? a : b); } int main () { int a; int b = 2; return max (a, b); }
No tags attached.
Issue History
2011-07-06 10:10yakobowskiNew Issue
2011-07-06 10:10yakobowskiStatusnew => assigned
2011-07-06 10:10yakobowskiAssigned To => pherrmann
2011-07-06 10:10yakobowskiNote Added: 0002010
2011-08-22 10:15pherrmannNote Added: 0002152
2011-08-22 10:15pherrmannStatusassigned => resolved
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2012-05-16 18:22signolesResolutionopen => fixed

Notes
(0002010)
yakobowski   
2011-07-06 10:10   
(Wp called with -wp-rte.)
(0002152)
pherrmann   
2011-08-22 10:15   
See svn 14739 for documentation update: RTE does not report usage of non initialized automatic variables. Would require a dataflow analysis to avoid an excessive number of generated annotations.