Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:47 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001044Frama-CPlug-in > Evapublic2014-03-13 15:57
Reporterpascal 
Assigned Toyakobowski 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001044: Smarter access to array of struct of array
DescriptionSmarter access to array of struct of array
TagsNo tags attached.
Attached Files
  • c file icon test1.c (455 bytes) 2011-12-11 00:06 -
    typedef struct {
      int i;
      short s;
      short pad;
      int* p;} T_STR1;
    
    #define CTE1 3
    
    #define CTE2 4
    
    typedef struct {
      int i;
      short s;
      short pad;
      T_STR1 ts[CTE2];
    } T_STR2;
    
    T_STR2 tab[CTE1];
    
    /*@
      @ requires 0<=index1<CTE1; 
      @ requires 0<=index2<CTE2; 
      @*/
    int f1(int index1, int index2, short ref)
    {
      short local;
      if (ref == tab[index1].ts[index2].s)
        {
          local =  tab[index1].ts[index2].s;
          return 0;
        }
    
      return -1;
    }
    
    c file icon test1.c (455 bytes) 2011-12-11 00:06 +

-Relationships
+Relationships

-Notes

~0004333

yakobowski (manager)

Implementation remains to be done in the logic. Unclear whether this is really useful or not.
+Notes

-Issue History
Date Modified Username Field Change
2011-12-10 23:39 pascal New Issue
2011-12-10 23:39 pascal Status new => assigned
2011-12-10 23:39 pascal Assigned To => pascal
2011-12-11 00:06 pascal File Added: test1.c
2013-10-10 20:51 yakobowski Assigned To pascal => yakobowski
2013-10-10 22:38 svn
2013-10-14 09:53 svn
2013-10-14 10:39 svn
2013-10-14 16:10 svn
2013-10-14 17:47 svn
2013-11-22 21:41 yakobowski Note Added: 0004333
2013-11-29 10:21 yakobowski Status assigned => resolved
2013-11-29 10:21 yakobowski Resolution open => fixed
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master 456dcee6
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master f936f2cc
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master cfcd6d3c
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master cf97d194
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master fe6286ee
2014-02-12 16:53 yakobowski Source_changeset_attached => framac stable/neon 456dcee6
2014-02-12 16:53 yakobowski Source_changeset_attached => framac stable/neon f936f2cc
2014-02-12 16:53 yakobowski Source_changeset_attached => framac stable/neon cfcd6d3c
2014-02-12 16:53 yakobowski Source_changeset_attached => framac stable/neon cf97d194
2014-02-12 16:53 yakobowski Source_changeset_attached => framac stable/neon fe6286ee
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History