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

[Frama-c-discuss] Lemma instantiation



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>