--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on October 2010 ---
> 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. ...