Combining Analyses Within Frama-C

Combinations of analysis techniques and tools can help verification engineers to achieve their goals. The Frama-C verification platform offers a large range of possibilities for combining its analyzers with each other or with external tools. This chapter provides an overview of several combinations with different objectives and levels of maturity. First, we show how model checking and Counterexample Guided Refinement Abstraction (CEGAR) are used with value analysis and deductive verification for proving statement contracts. Runtime assertion checking can provide the user with useful information by checking annotations on selected test inputs. Next, test generation can be used to classify alarms, explain proof failures and generate counterexamples. Finally, static techniques are capable to optimize test generation by detecting infeasible test objectives and thus avoiding a test generation tool to waste time by trying to cover them.