2021-02-27 11:41 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001348Frama-CPlug-in > wppublic2013-04-19 11:05
Reportersduprat 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001348: performance problem about number of fields in structure for struct equality properties
DescriptionFor the same case of assign of struct,
  - property about value of the assigned struct are proved for a small number of fields of struct
  - same property unproved with a larger struct (11 elts)
Additional InformationSee example in attached file
cmd:frama-c -wp source.c -wp-timeout 200
TagsNo tags attached.
Attached Files
  • c file icon source.c (606 bytes) 2013-01-13 01:14 -
    //frama-c -wp source.c -wp-timeout 200
    
    
    typedef struct {
      int c1;
    //  int c2;
    //  int c3;
    //  int c4;
    //  int c5;
    //  int c6;
    //  int c7;
    //  int c8;
    //  int c9;
      int p1[2];
    } T_S1;
    
    typedef struct {
      int c1;
      int c2;
      int c3;
      int c4;
      int c5;
      int c6;
      int c7;
      int c8;
      int c9;
      int p1[2];
    } T_S2;
    
    T_S1 GlobS1;
    T_S2 GlobS2;
    
    /*@
      assigns GlobS1, *s;
      ensures GlobS1 == *s;
    */
    void g1(T_S1* s);
    
    /*@
      ensures *p==GlobS1;
    */
    void f1(T_S1* p)
    {
      g1(p);
    }
    
    /*@
      assigns GlobS2, *s;
      ensures GlobS2 == *s;
    */
    void g2(T_S2* s);
    
    /*@
      ensures *p==GlobS2;
    */
    void f2(T_S2* p)
    {
      g2(p);
    }
    
    c file icon source.c (606 bytes) 2013-01-13 01:14 +

-Relationships
+Relationships

-Notes

~0003663

correnson (manager)

There is no problem with 'Typed' model.
L.

~0003664

sduprat (reporter)

that's right, that problem was originally found on Oxygen with typed, but is already fixed in the svn.
thanks.

~0003665

correnson (manager)

Fixed in the while
+Notes

-Issue History
Date Modified Username Field Change
2013-01-13 01:14 sduprat New Issue
2013-01-13 01:14 sduprat Status new => assigned
2013-01-13 01:14 sduprat Assigned To => correnson
2013-01-13 01:14 sduprat File Added: source.c
2013-01-15 19:21 correnson Note Added: 0003663
2013-01-16 00:55 sduprat Note Added: 0003664
2013-01-16 02:04 correnson Note Added: 0003665
2013-01-16 02:04 correnson Status assigned => resolved
2013-01-16 02:04 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