Frama-C Bug Tracking System - Frama-C
View Issue Details
0002311Frama-CPlug-in > wppublic2017-06-15 12:582017-06-15 12:58
Jochen 
correnson 
normaltextsometimes
assignedopen 
Phosphorus-20170501-beta1xubuntu
Frama-C 15-Phosphorus 
 
0002311: poor errors message texts for Hoare memory model checks
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).
No tags attached.
c memmodel_Hoare.c (115) 2017-06-15 12:58
https://bts.frama-c.com/file_download.php?file_id=1191&type=bug
Issue History
2017-06-15 12:58JochenNew Issue
2017-06-15 12:58JochenStatusnew => assigned
2017-06-15 12:58JochenAssigned To => correnson
2017-06-15 12:58JochenFile Added: memmodel_Hoare.c

There are no notes attached to this issue.