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: stephane.duprat at atosorigin.com (Stephane DUPRAT)
  • Date: Mon, 18 Oct 2010 10:55:20 +0200
  • In-reply-to: <AANLkTinDv06KN8UK58F432-oA_mAMPQcDqg2W=oJnsWm@mail.gmail.com>
  • References: <4CBB7020.9070904@atosorigin.com> <AANLkTimajz-L7cxPv0+11n=BEKKKrOp8PT0JLoRuvnRz@mail.gmail.com> <AANLkTinDv06KN8UK58F432-oA_mAMPQcDqg2W=oJnsWm@mail.gmail.com>
  I Pascal,

I forgot also the command line in my message, but you guessed that was 
with -lib-entry option !

Thank you for your answer,

St?phane


Le 18/10/2010 01:22, Pascal Cuoq a ?crit :
>> 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.
> ...
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
>