--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on January 2020 ---
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>