--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on May 2018 ---
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