2021-03-02 02:59 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000662Frama-CPlug-in > wppublic2011-04-13 15:28
Assigned Todargaye 
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 {
    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)
      ProgrammerSortie(EP_1, &G_uEpData1) ;
      return OK;
    c file icon source.c (1,375 bytes) 2011-01-07 16:23 +




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.


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.


sduprat (reporter)

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


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...


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


dargaye (developer)

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


correnson (manager)

In Revision 11223.


signoles (manager)

Fixed in WP 0.3 compatible with Frama-C Carbon.

-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