Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000072Frama-CPlug-in > jessiepublic2009-04-30 14:382010-02-12 09:00
Reporterbobot 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0000072: The specifications of statements are not translated
DescriptionNo vc are produced with this function. spec_statement.c : ============================== void myfun(int p){ p = 1; /*@ requires p==1; @ ensures \old(p)==p-1; @*/ p = 2; } ============================= spec_statement.jc: ======================== unit myfun(integer p) behavior default: assumes true; ensures (C_3 : true); { { (C_1 : (p = 1)); (C_2 : (p = 2)); (return ()) } } ========================
Additional Informationframa-c : 5186
TagsNo tags attached.
Attached Files

- Relationships
related to 0000370closedcmarche pragma JessieIntegerModel 

-  Notes
(0000679)
cmarche (developer)
2010-02-11 17:49

Partially fixed (see bug 0370), but their is still a bug with the handling of \old, with is wrongly interpreted in the pre-state of the function insteads of the pre-state of the statement

- Issue History
Date Modified Username Field Change
2009-04-30 14:38 bobot New Issue
2009-04-30 16:46 monate Status new => assigned
2009-04-30 16:46 monate Assigned To => cmarche
2010-02-11 17:49 cmarche Note Added: 0000679
2010-02-12 09:00 signoles Relationship added related to 0000370


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker