cannot proof the rte assertion in the loop for
ID0000699: This issue was created automatically from Mantis Issue 699. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000699 | Frama-C | Plug-in > wp | public | 2011-02-01 | 2011-02-02 |
| Reporter | liangliang | Assigned To | dargaye | Resolution | won't fix |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20101202-beta2 | Target Version | - | Fixed in Version | - |
Description :
When I run the commond: frama-c-gui -wp -wp-rte example.c and use alt-ergo, the rte assertion in the "loop for" can not be proved.