Gui unusable if value analysis degenerates
ID0000684: This issue was created automatically from Mantis Issue 684. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000684 | Frama-C | Graphical User Interface | public | 2011-01-24 | 2015-01-07 |
| Reporter | yakobowski | Assigned To | monate | Resolution | duplicate |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20101202-beta2 | Target Version | - | Fixed in Version | - |
Description :
If frama-c is started with -val, and the value analysis degenerates, the gui starts, then halts because of the exception of the value analysis. The error message "Degeneration occured:@\nresults are not correct for lines of code that can be reached from the degeneration point." of Eval.force_compute cannot be seen by the user, the gui exits before it is shown.
If frama-c is started without -val on the same code, and the value analysis is started manually, things go better. However the gui is left on a strange state where it is no longer possible to click reactively on the source code, and the right button menu is deactivated.
Additional Information :
Use the function below to force a degeneration. Ideally we would like to examine the state of the statement x++, which is before the degeneration.
void main () { int x = 1; double d; x++;
d = Frama_C_cos(1,2);
}