Saida

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

This is a plugin for Frama-C. Given an entry-point function with an ACSL contract, it infers ACSL contracts for helper functions, i.e. functions further down the call tree. Current version has been tested with Frama-C v31. Please note that the plugin is experimental and still under development so that no results are guaranteed.

Install TriCera

This plugin requires TriCera to be installed on your system, see: https://github.com/uuverifiers/tricera

Install and run Saida

• Installation:
  Register as plug-in using these commands (Ubuntu): dune build @install && dune install

• Execution:
  Run the plugin on file test.c as: frama-c -saida -saida-tricera-path <path-to-tricera> test.c
  where path-to-tricera is the path to the TriCera executable (tri). If no path is provided, the plugin will use tri in $PATH.

• Lib-entry option:
  Optionally, use the Frama-C lib-entry option to non-deterministically assign all global variables in TriCera before analysis, e.g.:
  frama-c -saida test.c -saida-tricera-path <path-to-tricera> -lib-entry

• Verification option:
  Use the -saida-wp option for running the -wp plugin to verify the inferred contracts and verify that the top-level contract for the main function can be verified by relying on inferred contract, use as:
  frama-c -saida -saida-tricera-path <path-to-tricera> -saida-wp test.c

Summary

The execution of the plugin can be summarized as:
Step 1: convert the top-level contract to a TriCera harness function
Step 2: Merge the harness function with the source code (this result is stored in /tmp/saida_harness_<file-name>.c)
Step 3: Run tricera on the result from step 2 (this result is stored in /tmp/saida_result_<file-name>.c)
Step 4: Merge the inferred contracts from step 3 with the source code (this result is stored in saida.out or file given by -saida-out=<file> option)
Step 5: (optional) Run the wp plugin on the result from step 4

Existing contracts

Saida keeps existing helper contracts in the TriCera input and adds inference placeholders only for helpers without contracts. Contracts on external functions (declarations without a body) are taken from Frama-C's merged specification and printed once with a matching prototype after the original source and before the verification harness. This keeps later typedefs and global declarations in scope, including when redeclarations rename parameters or use a newly introduced typedef. The original source is not modified; existing helper contracts are not duplicated in the output file.

An external contract is an assumption about code that is not available for verification, not a proof of its implementation. For subsequent Eva analysis, provide dependency information such as assigns state \from value; when needed. TriCera's supported ACSL subset still applies.

Development

A suitable development environment for the plugin is provided by the AutoDeduct toolchain docker image.

Please note that there are several TODO and FIX ME sprinkled around the code base. There are several test cases with TODO to indicate that their oracle file contains the result of an unsupported feature.

After adding tests, regenerate the ptest rules and run the comparisons:

frama-c-ptests -dune-alias runtest
dune build @install
dune test

tests/basic/external_contract.c reproduces issue #46. The related inline, redeclaration, declaration-order and negative tests check contract preservation. They require TriCera to report SAFE for valid callers and UNSAFE for the deliberately invalid caller. Some older tests intentionally record diagnostics for unsupported constructs; a passing ptest suite does not mean all those constructs are supported.

Limitations

The plugin is currently limited to programs/specifications following these rules:

• The entry-point function should contain a top-level contract containing a requires clause and an ensures clause.
• The non-entry-point functions has to be called somewhere from within the file
• Currently does not support floating points.
• Partial support for arrays and stack pointers.
• Heap pointers are generally supported (but bugs exist in some cases in the translation to ACSL).
• Does not support inference of contracts for functions with local static variables.
• In the ACSL contract, only ensures, requires, and supported behavior-assumes clauses over C expressions are supported, with the exception of certain uses of quantification: universal quantification is supported in the post-conditions, and existential quantification in the pre-condition. Other types of ACSL built-in or user defined constructs, such as logical functions and predicates, are not supported.
• Function behaviors with supported C-expression clauses are translated by keeping the default precondition as a harness assumption and guarding each named behavior's postconditions with its pre-state assumes and requires. Behavior-specific assigns, complete, and disjoint clauses are not translated.

Aside from the limitations listed above, many more limitations/bugs expected to exist.