Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002311Frama-CPlug-in > wppublic2017-06-15 12:582017-06-15 12:58
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeveritytextReproducibilitysometimes
StatusassignedResolutionopen 
PlatformPhosphorus-20170501-beta1OSxubuntuOS Version
Product VersionFrama-C 15 Phosphorus 
Target VersionFixed in Version 
Summary0002311: poor errors message texts for Hoare memory model checks
DescriptionRunning "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).
TagsNo tags attached.
Attached Filesc file icon memmodel_Hoare.c [^] (115 bytes) 2017-06-15 12:58 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2017-06-15 12:58 Jochen New Issue
2017-06-15 12:58 Jochen Status new => assigned
2017-06-15 12:58 Jochen Assigned To => correnson
2017-06-15 12:58 Jochen File Added: memmodel_Hoare.c


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker