--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on August 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] my first frama verification




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.