poor errors message texts for Hoare memory model checks
ID0002311: This issue was created automatically from Mantis Issue 2311. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002311 | Frama-C | Plug-in > wp | public | 2017-06-15 | 2017-06-15 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | text | Reproducibility | sometimes |
| Platform | Phosphorus-20170501-beta1 | OS | xubuntu | OS Version | - |
| Product Version | Frama-C 15-Phosphorus | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp -wp-rte -wp-model Hoare memmodel_Hoare.c" on the attached program produces the output:
... [rte] annotating function foo memmodel_Hoare.c:5:[wp] warning: Can not load value in Empty model memmodel_Hoare.c:5:[wp] warning: Can not load value in Empty model memmodel_Hoare.c:8:[wp] warning: Can not load value in Empty model memmodel_Hoare.c:8:[wp] warning: No validity memmodel_Hoare.c:4:[wp] warning: Can not load value in Empty model memmodel_Hoare.c:3:[wp] warning: No validity [wp] 4 goals scheduled ...
The name of the memory model is "Hoare" on the command line and in the WP manual (Sect.3.2, p.44), but it is called "Empty" in the error message output. Moreover, the message "No validity" should be expanded to be more understandable. As an additional convenience, Frama-C could mention in each message the variable it refers to ("x" resp. "*x") in all cases in the example).