--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on May 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Memory footprint



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