Needs for some refresh of the property status into the source code
ID0000792: This issue was created automatically from Mantis Issue 792. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000792 | Frama-C | Graphical User Interface | public | 2011-04-13 | 2011-04-13 |
| Reporter | patrick | Assigned To | monate | Resolution | duplicate |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
When running some long wp calculus required by the command line, unfolding of the source file freeze the status of the properties into the source code. The status isn't updated when ending the wp proofs.
Additional Information :
Command:
frama-c-gui -wp valinit.c
When the GUI opens the Frama-C window, unfold the source file valinit.c before the end of WP.