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] a value analysis case studie

  • Subject: [Frama-c-discuss] a value analysis case studie
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Mon, 18 Oct 2010 01:22:56 +0200
  • In-reply-to: <AANLkTimajz-L7cxPv0+11n=BEKKKrOp8PT0JLoRuvnRz@mail.gmail.com>
  • References: <4CBB7020.9070904@atosorigin.com> <AANLkTimajz-L7cxPv0+11n=BEKKKrOp8PT0JLoRuvnRz@mail.gmail.com>
> With these annotations, the value analysis proves the post-condition
> of init1, and takes advantage of the assertion to omit the alarm on
> the tab access.

I forgot the command-line:

frama-c -val -slevel 10 t.c -lib-entry -main f1
...
t.c:20:[value] Function init1, behavior default: postcondition got status valid
...
t.c:30:[value] Assertion got status unknown.
...