FIT

Note that this plugin is in an experimental state.

This plugin is licensed under the GPL2 license, see license headers in source code files and the full license in the LICENSE file.

PURPOSE

Semantic inference of auxiliary annotations in Frama-C. Frama-C is a software suite for analysis of C code. Importantly, Frama-C offers powerful value analysis and weakest precondition plugins over C source code.

The purpose of this Frama-C plugin is to automatically provide contract components for interacting with the WP plugin of Frama-C.

INSTALL

This plugin currently targets Frama-C 31.0, as declared in dune-project.

dune build @install
dune install

To run the test suite locally:

frama-c-ptests
dune build @ptests

USE

ISP analyzes C programs with existing ACSL contracts and generates auxiliary ACSL annotations for Frama-C/WP.

Depending on the program shape, ISP may emit:

• requires clauses for Eva-derived value ranges
• requires \valid_read(...) and requires \valid(...)
• requires \separated(...) for multiple mutated pointer arguments
• assigns clauses for mutated globals and pointer targets
• Eva-derived range ensures clauses
• arithmetic safety preconditions for simple single pointer updates such as *p = *p + 1

These arithmetic safety clauses are preconditions only. ISP does not infer relational pointer postconditions such as *p == \old(*p) + 1.

To run the plugin on file test.c, use:

frama-c -isp test.c

Options

• Use -isp-print if you want the result to be printed.
• Use -isp-print-file out.c if you want the result to be printed to file out.c.
• Use -isp-entry-point "function" if you want to use a different function as the entry point for the analysis than the default main.
• Use -isp-missing-helper-contracts to report functions that are reachable from contracted functions but do not have ACSL contracts themselves.
• Use -isp-missing-helper-contracts-json report.json to write that report as JSON for tools such as AutoDeduct.

THEORY

We perform semantic annotation of a program. We provide requires clauses and assigns clauses. Requires clauses are synthesized from possible run-time exceptions, where the Eva plugin provides semantic discharging of always true preconditions.

Our method is based on the value analysis of Frama-C, which can bound the possible values of program variables at different program points. In this way we can proceed to deduce necessary pre-conditions to prevent run-time errors in a program, bound the return values of functions, and realize a memory model specification for a program automatically.

The implementation uses a Frama-C visitor to collect accessed and mutated globals, pointer argument usage, function argument ranges, and simple arithmetic pointer mutations. Emission modules then add ACSL clauses based on the collected state and Eva results.

For reference, these are the Master's thesis reports by Skantz and Manjikian:

• Synthesis of annotations for partially automated deductive verification by Daniel Skantz
• Improving the Synthesis of Annotations for Partially Automated Deductive Verification by Hovig Manjikian

Limitations

C language limitations:

• Does currently not support complex expressions for indexing arrays, pointer arithmetic other than array indexing, nested pointers, or nested structs.
• Does not support programs with local static variables.

Regarding ACSL, support exist for requires, ensures, and assign clauses, as well as the behavior construct. Supports most ACSL operators (implication, nested inequalities, etc.), and the built-in predicates \valid and \valid_read. Other ACSL constructs and built-ins than the above are generally not supported currently.