An Exercise in Mind Reading: Automatic Contract Inference for Frama-C

Using tools for deductive verification, such as Frama-C, typically imposes substantial work overhead in the form of manually writing annotations. In this chapter, we investigate techniques for alleviating this problem by means of automatic inference of ACSL specifications. To this end, we present the Frama-C plugin SaidaSaida , which uses the assertion-based model checker TriCeraTriCera as a back-end tool for inference of function contracts. TriCeraTriCera transforms the program, and specifications provided as assume and assert statements, into a set of constrained Horn clauses (CHC), and relies on CHC solvers for the verification of these clauses. Our approach assumes that a C program consists of one entry-point (main) function and a number of helper functions, which are called from the main function either directly or transitively. SaidaSaida takes as input such a C  program, where the main function is annotated with an ACSL function contract, and translates the contract into a harness function, comprised mainly of assume and assert statements. The harness function, together with the original program, is used as input for TriCeraTriCera and, from the output of the CHC solver, TriCeraTriCera infers pre- and post-conditions for all the helper functions in the C program, and translates them into ACSL function contracts. We illustrate on several examples how SaidaSaida can be used in practice, and discuss ongoing work on extending and improving the plugin.