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


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.