RTE does not generate assertions for non initialized arguments
ID0000877: This issue was created automatically from Mantis Issue 877. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000877 | Frama-C | Plug-in > RTE | public | 2011-07-06 | 2012-05-16 |
| Reporter | yakobowski | Assigned To | pherrmann | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
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); }