2021-02-24 18:26 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000877Frama-CPlug-in > RTEpublic2012-05-16 18:22
Assigned Topherrmann 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000877: RTE does not generate assertions for non initialized arguments
DescriptionCalling 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);
TagsNo tags attached.
Attached Files




yakobowski (manager)

(Wp called with -wp-rte.)


pherrmann (reporter)

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.

-Issue History
Date Modified Username Field Change
2011-07-06 10:10 yakobowski New Issue
2011-07-06 10:10 yakobowski Status new => assigned
2011-07-06 10:10 yakobowski Assigned To => pherrmann
2011-07-06 10:10 yakobowski Note Added: 0002010
2011-08-22 10:15 pherrmann Note Added: 0002152
2011-08-22 10:15 pherrmann Status assigned => resolved
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2012-05-16 18:22 signoles Resolution open => fixed
+Issue History