2021-02-27 11:29 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001299Frama-CPlug-in > wppublic2013-04-19 11:05
Reportersduprat 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • c file icon report1.c (462 bytes) 2012-11-06 17:20 -
    
    
    //frama-c -wp -wp-print  -wp-byreference -wp-model Typed report1.c
    
    typedef struct {
      int c1;
      int c2;
    } T_S1;
    
    
    /*@
      assigns \nothing;
      ensures P1 : \result== p->c1;
    */
    int f1(T_S1* p)
    {
      return p->c1;
    }
    
    /*@
      ensures P1 : p->c1==2 ==> \result == 0;
      ensures P2 : p->c1!=2 ==> \result == -1;
    
      behavior b1:
        assumes p->c1==2;
        ensures b1_P1 : \result == 0;
    */
    int f2(T_S1* p)
    {
      int ret = 0;
    
      if (f1(p) != 2)
        ret=-1;
      
      return ret;
    }
    
    
    c file icon report1.c (462 bytes) 2012-11-06 17:20 +

-Relationships
+Relationships

-Notes

~0003661

sduprat (reporter)

Seems to be fixed on the SVN.
Thanks.
+Notes

-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
+Issue History