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

  • Subject: [Frama-c-discuss] Memory footprint
  • From: Frederic.Loulergue at nau.edu (Frederic Loulergue)
  • Date: Fri, 11 May 2018 12:23:38 -0700
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