--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on January 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Lemma instantiation



Hello again,

I’m a bit stuck with either how I’m designing my specification or how to instantiate lemmas properly. When I load the following in the GUI for use with TIP, I am unable to instantiate the axiom abs_semantics — it looks like I need to provide some memory for the union, but there are no such binders in scope.

(I am not sure if the program below is actually provable, but I don’t think that is important for my question.)

Thank you,
Alexander

union data {
  int i;
  float f;
};

struct val {
  int type;
  union data value;
};

struct stack {
   struct val *vals;
   unsigned int top;
   unsigned int max;
};

/*@ axiomatic abstraction {
      type value = Int(integer) | Float(float);
      type abs_stack = \list<value>;

      logic abs_stack abs(struct stack s);
      axiom abs_semantics:
        \forall struct stack s;
        TRIGGER: \length(abs(s)) == s.top &&
        (\forall integer i; (0 <= i < \length(abs(s))) ==>
          ( (s.vals[s.top - i - 1].type == 0 ==>
             TRIGGER: \nth(abs(s), i) == Int(s.vals[s.top - i - 1].value.i)) &&
            (s.vals[s.top - i - 1].type != 0 ==>
             TRIGGER: \nth(abs(s), i) == Float(s.vals[s.top - i - 1].value.f)) ));
        
    }
*/

/*@ ensures ( s1.top == s2.top &&
              s1.max == s2.max &&
              \valid(s1.vals + (0 .. s1.max-1)) &&
              \valid(s2.vals + (0 .. s2.max-1)) &&
              (\forall integer i; 
                 (0 <= i < s1.top) ==> (s1.vals[i] == s2.vals[i])) ) ==>
              abs(s1) == abs(s2);
*/
void some_function(struct stack s1, struct stack s2)
{
}

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200128/e082861e/attachment-0001.html>