--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on August 2015 ---
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.