--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] a value analysis case studie



  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
>
>