--- layout: fc_discuss_archives title: Message 55 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



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