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