2021-01-19 16:08 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002040Frama-CPlug-in > wppublic2016-01-26 08:52
Reporterjens 
Assigned Tocorrenson 
PriorityhighSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0002040: assumes clause and labels
DescriptionMy understanding of assumes clauses is that they refer to the pre-state of a function.
The attached example, however, works differently.
The function push_back has two disjoint behaviors that rely on the predicate "full".

The function push_back_twice is only verified if I add the label "Pre"
to the predicate "full" in the assumes clauses of function push_back.
I think this is a bug.
It should not be necessary to add this explicit label.
Additional InformationConcerns versions
Neon-20140301
Neon-20140301+dev-stance

I remember that Kim Völlinger had observed the same(?) problem in Oxygen and
that it was fixed in Fluorine.
TagsNo tags attached.
Attached Files
  • c file icon assumes_label.c (1,548 bytes) 2014-12-27 17:48 -
    typedef struct vector
    {
        int* addr;
        unsigned int sz;
        unsigned int cap;
    } vector;
    
    /*@
      predicate invariant{L}(vector* v) =
             v->sz <= v->cap &&
             \valid(v->addr + (0..v->cap-1)) &&
             \separated(v, v->addr + (0..v->cap-1));
    
      predicate full{L}(vector* v) = (v->sz == v->cap);
    */
    
    /*@
        requires \valid(v);
        requires invariant(v);
    
        assigns v->sz;
        assigns v->addr[v->sz];
    
        behavior enough_space:
            assumes !full{Pre}(v);
    
            assigns v->sz;
            assigns v->addr[v->sz];
    
            ensures \result == 1;
            ensures v->sz == \old(v->sz) + 1;
            ensures v->addr[\old(v->sz)] == x;
            ensures \forall integer i; 0 <= i < \old(v->sz)  ==>  v->addr[i] == \old(v->addr[i]);
    
       behavior no_space:
           assumes full{Pre}(v);
    
           assigns \nothing;
    
           ensures \result == 0;
    
       complete behaviors;
       disjoint behaviors;
    */
    int push_back(vector* v, int x)
    {
        if (v->sz < v->cap)
        {
            v->addr[v->sz] = x;
            v->sz++;
            return 1;
        }
        else
        {
            return 0;
        }
    }
    
    /*@
      requires \valid(v);
      requires invariant(v);
      requires v->sz + 1 < v->cap;
    
      assigns v->sz;
      assigns v->addr[v->sz];
      assigns v->addr[v->sz + 1];
    
      ensures v->sz == \old(v->sz) + 2;
      ensures v->addr[\old(v->sz)] == x;
      ensures v->addr[\old(v->sz) + 1] == x;
      ensures \forall integer i; 0 <= i < \old(v->sz)  ==>  v->addr[i] == \old(v->addr[i]);
    */
    void push_back_twice(vector* v, int x)
    {
        push_back(v, x);
        //@ assert !full(v);
        push_back(v, x);
    }
    
    
    c file icon assumes_label.c (1,548 bytes) 2014-12-27 17:48 +

-Relationships
+Relationships

-Notes

~0006007

correnson (manager)

Fixed normalization of `Here` in assumes when prepended to ensures.

~0006008

correnson (manager)

@Jens : this bug was never fixed before ; probably Kim found a workaround when working with Fluorine...
+Notes

-Issue History
Date Modified Username Field Change
2014-12-27 17:48 jens New Issue
2014-12-27 17:48 jens Status new => assigned
2014-12-27 17:48 jens Assigned To => correnson
2014-12-27 17:48 jens File Added: assumes_label.c
2015-06-29 17:46 correnson Status assigned => acknowledged
2015-08-19 10:38 correnson Note Added: 0006007
2015-08-19 10:38 correnson Status acknowledged => resolved
2015-08-19 10:38 correnson Resolution open => fixed
2015-08-19 10:39 correnson Note Added: 0006008
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed
+Issue History