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] Memory footprint

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