Conclusion

Now that you should know how to analyze an application, it is important to insist on how it is important to put things together and check all the hypotheses.

If there is only one analysis, it is quite easy to check. The results rely on:

  • the context defined by the entry point,
  • the assigns and ensures properties of the external functions because they cannot be checked,
  • all the other annotations that are not either valid according the value analysis or proved by WP. If there are several analyses, the results of each of one rely on the same hypotheses than above, but there are more things to check:
  • the WP proofs doesn’t depend on the context, so they can be done only once, IF the functions are the same across the analyses (not modified through a macro for instance),
  • to be valid according to the value analysis, a property must have this status in ALL the analyses,
  • when splitting, remember that the context of the function analysis must represent all its precondition (see figure in Pre-conditions of a Defined Function).

To be fully verified in the given context all the hypotheses above must have a clear justification for lack of formal verification.