Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>