Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] my first frama verification
- Subject: [Frama-c-discuss] my first frama verification
- From: anne.pacalet at free.fr (Anne Pacalet)
- Date: Fri, 21 Aug 2015 08:43:40 +0200
- In-reply-to: <CAGSRWbgk8sbO4DKZ-ij8jbDALBgt8e7K4dAto-puDQZqbu+76Q@mail.gmail.com>
- References: <CAGSRWbgk8sbO4DKZ-ij8jbDALBgt8e7K4dAto-puDQZqbu+76Q@mail.gmail.com>
Le 21/08/2015 00:13, Tim Newsham a écrit : > Are there some strategies for > using the value analysis in a more modular way that you would > recommend (for example, if I could somehow prove that hmac > was safe, in isolation, and then ommit the hmac implementation > from the whole program analysis). Yes, you can do so. You would have to: - give a specification to the function (requires + assigns/from + ensures properties) - write a driver to analyze the function. Be careful to analyze it in a context that includes ALL the behaviors specified by the preconditions (requires) - check that the properties are verified in this analyze - then go back to your main analyze and use the -val-use-spec option. This will check that the preconditions are verified, and assume the postconditions instead of analyzing the function. > What about other plugins to frama-c and why3? Beside Jessie, you could also try the WP plug-in. Hope this helps. Anne.
- References:
- [Frama-c-discuss] my first frama verification
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] my first frama verification
- Prev by Date: [Frama-c-discuss] headers question
- Next by Date: [Frama-c-discuss] my first frama verification
- Previous by thread: [Frama-c-discuss] my first frama verification
- Next by thread: [Frama-c-discuss] my first frama verification
- Index(es):