2021-02-27 11:04 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000793Frama-CPlug-in > wppublic2013-04-19 11:05
Reporterpatrick 
Assigned Todargaye 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0000793: time too long even with -wp-timeout 1
DescriptionThe PO is quickly computed, but the proof seems to take a llong time, but -wp-timeout 1 has no effect.
Additional InformationRevision: 12840
> frama-c valinit.c -wp -wp-prop p4 -wp-proof alt-ergo -wp-timeout 1
TagsNo tags attached.
Attached Files
  • c file icon valinit.c (3,663 bytes) 2011-04-13 13:44 -
    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} ;
    
    struct st { int b ; int a ; } ;
    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 p0:   ok:x==3;
      @ ensures       ok:t1[0]==3;
      @ ensures       ok:t15[2]==0;
      @ ensures p1: todo: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 p4: todo: 
                  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 (3,663 bytes) 2011-04-13 13:44 +

-Relationships
+Relationships

-Notes

~0001780

patrick (developer)

The problem comes from a combinational explosion when expanding the 'let' constructs before calling the prover.

~0001916

dargaye (developer)

from alt-ergo

~0003753

correnson (manager)

Timeout 12s with wp-par 1 is now ok.
Using -wp-model ref makes each PO discharged in less than 4s.

~0003754

correnson (manager)

Together with issue 0000794.
+Notes

-Issue History
Date Modified Username Field Change
2011-04-13 13:44 patrick New Issue
2011-04-13 13:44 patrick Status new => assigned
2011-04-13 13:44 patrick Assigned To => dargaye
2011-04-13 13:44 patrick File Added: valinit.c
2011-04-14 09:56 patrick Note Added: 0001780
2011-05-20 13:43 dargaye Note Added: 0001916
2011-05-20 13:43 dargaye Status assigned => closed
2011-05-20 13:43 dargaye Resolution open => fixed
2013-03-12 13:18 correnson Note Added: 0003753
2013-03-12 13:18 correnson Note Added: 0003754
2013-03-12 13:18 correnson Status closed => resolved
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
+Issue History