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