--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on May 2018 ---
Hi, Unfortunately, for now, WP does not generate frame lemmas from reads clause for proving your `Unchanged` assertion. Indeed it would be a nice feature. However, you can write it yourself, with something like: lemma unchanged_f{A,B} : \forall args, (\forall b, P ==> \at( s , A ) == \at( s , B )) ==> f{A}(args) == f{B}(args) ; The problem is that triggers for such a lemma are sometimes difficult to infer (for Alt-Ergo and other SMT solvers). Hence, probably you need to instanciate such lemmas by hand (using the TIP or Coq). For your information, we are also working on new memory models based on user-declared memory regions in order to help such proofs. But it will *not* be available soon⦠:-) Regards, L. > Le 11 mai 2018 à 21:23, Frederic Loulergue <Frederic.Loulergue at nau.edu> a écrit : > > Hello, > > I use WP. I have a function f with a reads clause in the form { s | b ; P }, and > > Assign: > > *x := e; > > //@ assert Unchanged: f(args) == f{Assign}(args); > > Unchanged is not proved. > > What is the best way to assert that "the memory changes are disjoint from the declared footprint" so that the assertion Unchanged can be proved? > > Thanks, > > Frederic > > > -- > Dr. Frederic Loulergue > Professor > School of Informatics, Computing, and Cyber Systems > Northern Arizona University > Home: http://nau.edu/SICCS/Faculty/Frederic-Loulergue > Phone: +1 928-523-5044 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss