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

[Frama-c-discuss] WP RTE mem_access condition is Unknown



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