2021-02-27 11:37 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001316Frama-CPlug-in > wppublic2014-02-12 16:58
Reportersduprat 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001316: false property proved intTyped (if confirmed)
DescriptionIn the attached exemple, the property OUT_ko3 of f2b is proved while it seems to be not a true property.
The problem is in Typed and not in Store.

The problem is also in SVN 20767.
Additional Information//frama-c -wp rp2.c -wp-byreference -wp-model Store --> OK
//frama-c -wp rp2.c -wp-byreference -wp-model Typed --> f1b/OUT_ko3 is proved
TagsNo tags attached.
Attached Files
  • c file icon rp2.c (591 bytes) 2012-11-22 21:46 -
    //frama-c -wp rp2.c -wp-byreference -wp-model Store  --> OK
    //frama-c -wp rp2.c -wp-byreference -wp-model Typed  --> f1b/OUT_ko3 is proved
    
    
    /*@
      assigns \result;
      ensures \result == *p;
    */
    extern  int f1b( int *p);
    
    /*@
      @ ensures OUT_ko2: *s1 == 33;
      @ ensures OUT_ko3: *s1 == \old(*s1);
      @*/
     int f2b(
       int * s1,
       int * s2)
    {
    
       *s1 = f1b(s2);
    
       /* return code */
       return 0 ;
    }
    extern  int f1b( int *p);
    
    
    /*@
      @ ensures OUT_ko2: *s1 == 33;
      @ ensures OUT_ko3: *s1 == \old(*s1);
      @*/
     int f2c(
       int * s1,
       int v)
    {
    
       *s1 = v;
    
       /* return code */
       return 0 ;
    }
    
    c file icon rp2.c (591 bytes) 2012-11-22 21:46 +

-Relationships
+Relationships

-Notes

~0004599

correnson (manager)

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2012-11-22 21:46 sduprat New Issue
2012-11-22 21:46 sduprat Status new => assigned
2012-11-22 21:46 sduprat Assigned To => correnson
2012-11-22 21:46 sduprat File Added: rp2.c
2012-12-07 13:18 svn
2012-12-07 13:18 svn Status assigned => resolved
2012-12-07 13:18 svn Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
2013-12-19 01:11 correnson Source_changeset_attached => framac master c4b84705
2014-02-12 16:53 correnson Source_changeset_attached => framac stable/neon c4b84705
2014-02-12 16:58 correnson Note Added: 0004599
2014-02-12 16:58 correnson Status closed => resolved
+Issue History