2021-01-22 20:11 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000794Frama-CPlug-in > wppublic2013-04-19 11:05
Reporterpatrick 
Assigned Tocorrenson 
PrioritynormalSeverityfeatureReproducibilityhave not tried
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0000794: initial value of strings
DescriptionWP is unable to proof properties on initial value of a string.
That comes from the uncompleteness of the generated PO; there is nothing about the initial value of the string.
Additional Information> frama-c -wp -wp-prop p0 valinit.c -wp-proof alt-ergo
...
[wp] [Alt-Ergo] Goal store_main_post_9_p0 : Timeout


TagsNo tags attached.
Attached Files
  • c file icon valinit.c (4,137 bytes) 2011-04-14 16:11 -
    int x = 3 ;
    int t1[1] = {3} ;
    int t2[2] = {3,4} ;
    int t3[3] = {3,4} ;
    int t15[15] = {3} ;
    int t20[20] = {3} ;
    int t40[40] = {0,1,2,3,4,5,6,7,8,9,
    	      10,11,12,13,14,15,16,17,18,19,
    	      20,22,22,33,34,35,36,37,38,39,
    	      30,33,33,33,34,35,36,37,38,39} ;
    int t50[50] = {0,1,2,3,4,5,6,7,8,9,
    	      10,11,12,13,14,15,16,17,18,19,
    	      20,22,22,33,34,35,36,37,38,39,
    	      30,33,33,33,34,35,36,37,38,39,
    	      40,44,42,43,44,45,46,47,48,49} ;
    int t60[60] = {0,1,2,3,4,5,6,7,8,9,
    	      10,11,12,13,14,15,16,17,18,19,
    	      20,22,22,33,34,35,36,37,38,39,
    	      30,33,33,33,34,35,36,37,38,39,
    	      40,44,42,43,44,45,46,47,48,49,
    	      50,55,52,53,55,55,56,57,58,59} ;
    
    unsigned char uca = 'a' ;
    int *px = &x, **ppx = &px, *pt4 = &t40[4] ;
    char * str = "str" ;
    
    struct st { int b ; int a ; } ;
    struct st vs = { 2, 1 } ;
    struct st ts[56] = {
      4, 1, 6, 1, 7, 1, 1, 2, 1, 1, 8, 1, 2, 2, 12, 2, 10, 1, 6, 2, 
      9, 1, 3, 2, 4, 2, 5, 2, 6, 2, 7, 2, 9, 2, 10, 1, 2, 1, 10, 2, 
      11, 1, 12, 1, 12, 2, 16, 2, 18, 2, 19, 2, 30, 2, 31, 1, 12, 1, 9, 2, 
      11, 1, 20, 1, 12, 2, 11, 1, 21, 2, 5, 1, 16, 1, 8, 1, 9, 1, 22, 1, 
      22, 1, 22, 2, 22, 2, 22, 2, 22, 1, 22, 1, 22, 1, 22, 2, 22, 2, 22, 1, 
      22, 1, 22, 2, 22, 1, 22, 2, 22, 2, 22, 2
    };
    
    /*@ ensures       ok: x==3;
      @ ensures       ok: uca=='a';
      @ ensures       ok: px==&x;
      @ ensures       ok: *px==3;
      @ ensures       ok: ppx==&px;
      @ ensures       ok: *ppx==&x;
      @ ensures       ok: pt4==&t40[4];
      @ ensures       ok: *pt4==4;
      @ ensures p0: str[0]=='s' && str[1]=='t' && str[2]=='r' && str[3]=='\0';
      @ ensures       ok: t1[0]==3;
      @ ensures       ok: t15[2]==0;
      @ ensures p1: bts788: t20[2]==0;
      @ ensures       ok: \forall integer i ; 0<i<40 ==> t40[i]>0;
      @ ensures       ok: \forall integer i ; 0<i<50 ==> t50[i]>0;
      @ ensures p2: todo: \forall integer i ; 0<i<60 ==> t60[i]>0;
      @ ensures p3: todo: \forall integer i ; 0<i<60 ==> t60[i]>0;
      @ ensures       ok: vs.a == 1 && vs.b == 2;
      @ ensures p4: bts793: 
                  ts[0].b==4 && ts[0].a==1 && ts[1].b==6 && ts[1].a==1 && 
                  ts[2].b==7 && ts[2].a==1 && ts[3].b==1 && ts[3].a==2 && 
                  ts[4].b==1 && ts[4].a==1 && ts[5].b==8 && ts[5].a==1 && 
                  ts[6].b==2 && ts[6].a==2 && ts[7].b==12 && ts[7].a==2 && 
                  ts[8].b==10 && ts[8].a==1 && ts[9].b==6 && ts[9].a==2 && 
                  ts[10].b==9 && ts[10].a==1 && ts[11].b==3 && ts[11].a==2 && 
                  ts[12].b==4 && ts[12].a==2 && ts[13].b==5 && ts[13].a==2 && 
                  ts[14].b==6 && ts[14].a==2 && ts[15].b==7 && ts[15].a==2 && 
                  ts[16].b==9 && ts[16].a==2 && ts[17].b==10 && ts[17].a==1 && 
                  ts[18].b==2 && ts[18].a==1 && ts[19].b==10 && ts[19].a==2 && 
                  ts[20].b==11 && ts[20].a==1 && ts[21].b==12 && ts[21].a==1 && 
                  ts[22].b==12 && ts[22].a==2 && ts[23].b==16 && ts[23].a==2 && 
                  ts[24].b==18 && ts[24].a==2 && ts[25].b==19 && ts[25].a==2 && 
                  ts[26].b==30 && ts[26].a==2 && ts[27].b==31 && ts[27].a==1 && 
                  ts[28].b==12 && ts[28].a==1 && ts[29].b==9 && ts[29].a==2 && 
                  ts[30].b==11 && ts[30].a==1 && ts[31].b==20 && ts[31].a==1 && 
                  ts[32].b==12 && ts[32].a==2 && ts[33].b==11 && ts[33].a==1 && 
                  ts[34].b==21 && ts[34].a==2 && ts[35].b==5 && ts[35].a==1 && 
                  ts[36].b==16 && ts[36].a==1 && ts[37].b==8 && ts[37].a==1 && 
                  ts[38].b==9 && ts[38].a==1 && ts[39].b==22 && ts[39].a==1 && 
                  ts[40].b==22 && ts[40].a==1 && ts[41].b==22 && ts[41].a==2 && 
                  ts[42].b==22 && ts[42].a==2 && ts[43].b==22 && ts[43].a==2 && 
                  ts[44].b==22 && ts[44].a==1 && ts[45].b==22 && ts[45].a==1 && 
                  ts[46].b==22 && ts[46].a==1 && ts[47].b==22 && ts[47].a==2 && 
                  ts[48].b==22 && ts[48].a==2 && ts[49].b==22 && ts[49].a==1 && 
                  ts[50].b==22 && ts[50].a==1 && ts[51].b==22 && ts[51].a==2 && 
                  ts[52].b==22 && ts[52].a==1 && ts[53].b==22 && ts[53].a==2 && 
                  ts[54].b==22 && ts[54].a==2 && ts[55].b==22 && ts[55].a==2 ;
    
    
    
    */
    void main (void) { }
    
    
    
    
    c file icon valinit.c (4,137 bytes) 2011-04-14 16:11 +

-Relationships
+Relationships

-Notes

~0001929

dargaye (developer)

The constant of type string are not yet implemented for the moment in the Wp plugin's.

~0003751

correnson (manager)

This bug is now corrected.
You must set the option -wp-literals to get the value of string literals axiomatized.

~0003752

correnson (manager)

SVN 21663
+Notes

-Issue History
Date Modified Username Field Change
2011-04-14 16:11 patrick New Issue
2011-04-14 16:11 patrick Status new => assigned
2011-04-14 16:11 patrick Assigned To => dargaye
2011-04-14 16:11 patrick File Added: valinit.c
2011-05-27 14:17 dargaye Note Added: 0001929
2011-05-27 14:31 dargaye Severity minor => feature
2011-07-04 14:37 dargaye Assigned To dargaye => correnson
2013-03-12 13:08 correnson Note Added: 0003751
2013-03-12 13:11 correnson Note Added: 0003752
2013-03-12 13:11 correnson Status assigned => resolved
2013-03-12 13:11 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