--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on May 2014 ---
On Fri, 2014-05-23 at 22:33 +0200, Pascal Cuoq wrote: > You should provide function b() with a contract, otherwise, how can the WP > plug-in know what it does? The assigns clause would be the important part > of that contract, since it would tell that the x being dereferenced is the > same as the x that the precondition says is valid. That worked! Thanks very much. (I added "assigns \nothing" to the function b and "assigns *x" to the function a, if anyone is curious.) Mansour