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] WP RTE mem_access condition is Unknown

  • Subject: [Frama-c-discuss] WP RTE mem_access condition is Unknown
  • From: mansourmoufid at gmail.com (Mansour Moufid)
  • Date: Fri, 23 May 2014 17:47:44 -0400
  • In-reply-to: <CAOH62Jgx-Wd0dKEan3zOtmRqL2GikaahE4tzPO64=OcKKWJ1hQ@mail.gmail.com>
  • References: <1400876442.8745.6.camel@one> <CAOH62Jgx-Wd0dKEan3zOtmRqL2GikaahE4tzPO64=OcKKWJ1hQ@mail.gmail.com>
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