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

[Frama-c-discuss] Lemma Selection



Hi all,

I have the following (silly, meaningless) program:

typedef struct foo_s {
    int x;
    int y;
} foo_t;

/*@ axiomatic funcs {
  @   logic int func1(foo_t x);
  @   logic int func2(int x);
  @   }
  @   */

/*@ lemma foo:
  @   \forall foo_t f1;
  @   \forall foo_t f2;
  @   func1(f2) == func1(f1) ==>
  @   func1(f1) == func2(func1(f2));
  @*/

//@assigns pFoo->x, pFoo->y;
void boo(foo_t *pFoo);

//@ requires \valid(pFoo);
void goo(foo_t *pFoo) {
    //@ ghost foo_t f = *pFoo;
 PRE:
    boo(pFoo);
    //@ ghost foo_t g = *pFoo;
    //@ assert func1(f) == func2(func1(g));
}

When I load this in the frama-c gui and try to prove the assertion, I’m surprised that I can not select the lemma `foo`. How does frama-c/wp decide which lemmas are related to the term?

Thanks,
Alexander

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