2021-03-02 02:59 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000662Frama-CPlug-in > wppublic2011-04-13 15:28
Reportersduprat 
Assigned Todargaye 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFrama-C Carbon-20110201Fixed in VersionFrama-C Carbon-20110201 
Summary0000662: warning: Degenerated goal
Descriptionwarning degenerated goal is raised with this source example containing unions.
ensures are unproved.
Additional Informationframa-c -wp -pp-annot -wp-model Store -wp-proof alt-ergo -wp-split *.c


[wp] warning: Degenerated goal store_f1_post_5_P1 (1 warning)
[wp] warning: Degenerated goal store_f1_post_6_P2 (2 warnings)
[wp] warning: Degenerated goal store_f1_post_7_P3 (3 warnings)
[wp] [Alt-Ergo] Goal store_f1_post_7_P3 : Unknown
[wp] [Alt-Ergo] Goal store_f1_post_6_P2 : Unknown
[wp] [Alt-Ergo] Goal store_f1_post_5_P1 : Unknown
TagsNo tags attached.
Attached Files
  • c file icon source.c (1,375 bytes) 2011-01-07 16:23 -
    typedef unsigned int T_W32;
    
    typedef enum {
      ID_PROGRAMMERSORTIE,
      ID_ATTENDREDELAI,
      ID_VERIFIERSORTIE,
      ID_DECLARERPANNE} T_IF_FUNC;
    
    typedef enum {OK, KO} T_RES ;
    
    typedef enum {EP_1, EP_2} T_EP ;
    
    typedef enum {NO_ERROR, ERR_1, ERR_2} T_ERRORS ;
    
    
    
    
    
    
    typedef struct {
      unsigned char data[1000];
      int i;
    } T_DATA_CONF;
    
    typedef union {
      unsigned char CONF[120];
      int i;
    } T_CMD;
    
    typedef struct {
      int id1;
      int id2;
    } T_ERREUR;
    
    typedef struct {
      int index;
      int desc1;
      int desc2;
    } T_PANNE;
    
    
    
    
    
    //@ghost extern T_W32 __ProgrammerSortie_cpt; 
    //@ghost extern T_EP  __ProgrammerSortie_p1[]; 
    //@ghost extern T_CMD  __ProgrammerSortie_p2[]; 
    
    
    /*@ 
        requires __ProgrammerSortie_cpt >= 0;
    
        assigns __ProgrammerSortie_cpt;
        assigns __ProgrammerSortie_p1[__ProgrammerSortie_cpt];
    
        ensures __ProgrammerSortie_cpt == (\old(__ProgrammerSortie_cpt + 1));
        ensures __ProgrammerSortie_p1[\old(__ProgrammerSortie_cpt)] == ep;
        ensures __ProgrammerSortie_p2[\old(__ProgrammerSortie_cpt)] == *cmd;
    */
    extern void ProgrammerSortie(const T_EP ep, const T_CMD * const cmd);
    
    
    
    T_CMD G_uEpData1;
    
    /*@
      requires __ProgrammerSortie_cpt == 0; 
      ensures  P1 : \result ==  OK;
      ensures  P2 : __ProgrammerSortie_p2[0].i==33;
      ensures  P3 : G_uEpData1.i==33;
      @*/
    T_RES f1(void)
    {
      G_uEpData1.i=33;
      ProgrammerSortie(EP_1, &G_uEpData1) ;
      return OK;
    }
    
    c file icon source.c (1,375 bytes) 2011-01-07 16:23 +

-Relationships
+Relationships

-Notes

~0001367

dargaye (developer)

The memory model store does not support union.
Using -wp-print, you can see the warning details.

Instead of rejected the PO containing "union" feature, we produce a degenerated P0.
Then, if the "union" part of the PO is not crucial to the PO, it can be proved.
In this example, this is not the case.

~0001368

Anne (reporter)

With -wp-model Hoare, it stops because :
  Reason: unsupported cast from pointer (T_CMD) to pointer (T_CMD const)
I guess Hoare should be able to handle this kind of cast.
I will have a look : probably something to do, here.

~0001369

sduprat (reporter)

Well, It could be a feature.
union is a little bit supported : if we comment call of ProgrammerSortie, we can prove P3.

~0001370

Anne (reporter)

After a small fix about the cast in Hoare, I get :
[wp] [Alt-Ergo] Goal hoare_f1_post_7_P3_part1 : Valid
[wp] [Alt-Ergo] Goal hoare_f1_post_7_P3_part2 : Valid
[wp] [Alt-Ergo] Goal hoare_f1_post_6_P2_part1 : Valid
[wp] [Alt-Ergo] Goal hoare_f1_post_5_P1 : Valid
[wp] [Alt-Ergo] Goal hoare_f1_post_6_P2_part2 : Unknown

It seems that the last one should also be proved, but there is a problem in [union] comparison... I investigate further...

~0001372

Anne (reporter)

Ok : I fixed the problem of union comparison in rev 11223...
$ frama-c -wp -wp-model Hoare -wp-proof alt-ergo -wp-split source.c

[wp] [Alt-Ergo] Goal hoare_f1_post_7_P3_part1 : Valid
[wp] [Alt-Ergo] Goal hoare_f1_post_6_P2_part2 : Valid
[wp] [Alt-Ergo] Goal hoare_f1_post_6_P2_part1 : Valid
[wp] [Alt-Ergo] Goal hoare_f1_post_5_P1 : Valid
[wp] [Alt-Ergo] Goal hoare_f1_post_7_P3_part2 : Valid

~0001439

dargaye (developer)

I let Anne conclude if this bts has to be closed, since for Store it is out of scope.

~0001448

correnson (manager)

In Revision 11223.

~0001762

signoles (manager)

Fixed in WP 0.3 compatible with Frama-C Carbon.
+Notes

-Issue History
Date Modified Username Field Change
2011-01-07 16:23 sduprat New Issue
2011-01-07 16:23 sduprat Status new => assigned
2011-01-07 16:23 sduprat Assigned To => dargaye
2011-01-07 16:23 sduprat File Added: source.c
2011-01-07 16:35 dargaye Note Added: 0001367
2011-01-07 16:47 Anne Note Added: 0001368
2011-01-07 16:50 sduprat Note Added: 0001369
2011-01-07 17:20 Anne Note Added: 0001370
2011-01-10 14:43 Anne Note Added: 0001372
2011-01-28 11:42 correnson Target Version => Frama-C Carbon-20110201
2011-01-31 09:18 dargaye Note Added: 0001439
2011-02-01 17:04 correnson Note Added: 0001448
2011-02-01 17:04 correnson Status assigned => resolved
2011-02-01 17:04 correnson Fixed in Version => Frama-C Carbon-20110201
2011-02-01 17:04 correnson Resolution open => fixed
2011-04-13 15:28 signoles Note Added: 0001762
2011-04-13 15:28 signoles Status resolved => closed
+Issue History