Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001299Frama-CPlug-in > wppublic2012-11-06 17:202013-04-19 11:05
Reportersduprat 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001299: unproven property used in a behavior in Typed model
DescriptionIn the attached example, the b1_P1 property is unproven while the equivalent whithout the use of behavior is well proven.

This is in case if Typed model. In Store, all is proved.

Seeing the generated goals, perhaps a lack of relation between Mint_1 and Mint_0?

Or a problem in my assigns ?
In case of problem, is there any workaround ?


Regards.

St├ęphane
Additional InformationUsed with Alt-Ergo 0.94.

command used :
//frama-c -wp -wp-print -wp-byreference -wp-model Typed report1.c
TagsNo tags attached.
Attached Filesc file icon report1.c [^] (462 bytes) 2012-11-06 17:20 [Show Content]

- Relationships

-  Notes
(0003661)
sduprat (reporter)
2013-01-12 23:33

Seems to be fixed on the SVN.
Thanks.

- Issue History
Date Modified Username Field Change
2012-11-06 17:20 sduprat New Issue
2012-11-06 17:20 sduprat Status new => assigned
2012-11-06 17:20 sduprat Assigned To => correnson
2012-11-06 17:20 sduprat File Added: report1.c
2013-01-12 23:33 sduprat Note Added: 0003661
2013-01-15 19:23 correnson Status assigned => resolved
2013-01-15 19:23 correnson Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker