--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on January 2020 ---
I think I have identified the problem â the error is that `abs_stack` should be marked as reading `vals`, is that correct? Thanks again, Alexander > On Jan 28, 2020, at 12:56 PM, Alexander Bakst <abakst at galois.com> wrote: > > 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/20200129/7987f832/attachment-0001.html>