--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on August 2008 ---
Hi, Adding assert annotations could be helpfull to refine value analysis. But if the assertion could not be verified during the value analysis, we have a message that indicates "Assertion got status unknown". So, I feel the need to verify that assertion to have a more complete verification... Thanks to jessie plugin, and by means of other annotations, I succeed in proving all these annotations. This is a good collaboration of the different plugins. But theses operations have been made in 2 independent steps that are value analysis and proof with jessie. I tried to use frama-c with the two plugins activated with a cmd like that : frama-c-gui -val -lib-entry -jessie-analysis -jessie-gui -jessie-int-model exact exemple.c but I don't find in messages of the value analysis the status of annotations resulting from jessie analysis. Is it possible ? If not, do you think it's conceivable ? small exemple in attached file regards, St?phane Duprat -------------- next part -------------- A non-text attachment was scrubbed... Name: exemple.c Type: text/x-csrc Size: 635 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20080820/c20752ee/exemple.c