ACSL Properties

This chapter explains how to introduce ACSL properties to a project.

ACSL is the specification language employed in TrustInSoft Analyzer. ACSL properties can be used to specify functions (as seen in Write a Specification) and to guide the analysis by adding local annotations, such as assertions or loop invariants, which may help in removing false alarms (as seen in Remove Alarms by Adding Annotations).

There are two ways to insert ACSL properties in a project:

  • through inlining: putting ACSL properties directly in the analyzed application’s source code,
  • through importing: writing ACSL properties into external files and then loading these files from the command line when running the analysis.

Inline ACSL Properties

One way to add ACSL annotations to a project is to write them directly in the source code in special comments:

  • either standard C style comments: /*@ ... */,
  • or one line C++ style comments: //@ ....

There are several kinds of properties and they all need to be placed in an appropriate place in the source code:

  • Function specifications (described in Write a Specification) must be inserted either before the function itself or before the function’s declaration.
  • Local properties (described in Remove Alarms by Adding Annotations):
    • assertions must be inserted at the program point where they apply,
    • loop properties must be inserted just before the loop they apply to.

For more information about the ACSL language, please refer to the ACSL Documentation.

Import ACSL Properties

For many reasons it is usually preferable to avoid modifying the source code which is analyzed, as introducing changes to the application’s code can lead to difficulties in comparing it with the original version. For example, adding new properties alters the line numbering in a file, which makes it impossible to report problems with the original source line number.

The ACSLimporter plug-in makes it possible to write the ACSL properties into separate files and then import them for the analysis. The syntax of such files looks like this:

function <function-name>:
    requires <pre-name-1>: <pre-definition-1>;
    assigns <assigns-definition-1>;
    ensures <post-name-1>: <post-definition-1>;

  at L1: assert <assert-name-1a>: <assert-definition-1a>;
  at L1: assert <assert-name-1b>: <assert-definition-1b>;
  at L2: assert <assert-name-2>: <assert-definition-2>;

  at loop 1:
    loop invariant <inv-name-1a>: <inv-definition-1a>;
    loop invariant <inv-name-1b>: <inv-definition-1b>;

Of course, the <...> parts should be substituted by specific names and definitions.

Depending on the organization of the project, it might be better to put all the properties in a single ACSL file or to split them throughout several files. If the properties concerning the same function appear in different files, the specifications are merged.

To load the property files, so that they are taken into account during the analysis, the -acsl-import <file.acsl> option has to be specified for each concerned ACSL file.

Naming the Annotations

Giving a unique name to each annotation permits referring to it easily later on. Moreover, it makes the result files a lot clearer and more readable: when mentioning a particular annotation they will use its name instead of the corresponding file name and line number.

Using standard naming conventions is highly recommended. Some tools require particular naming of assertions to properly check that everything have been verified at the end of the analysis.

The proposed naming conventions are:

  • To choose a unique short prefix for annotations concerning each function (example: add_).
  • To include a letter that indicates the kind of each property (e.g. first requires property for function add could be then named add_r1). (However, this not really necessary if the name is always used together with the corresponding keyword, like for example: requires add_r1, ensures add_e2, etc.)
  • To use a suffix informing about the way each property is verified. For instance:
    • add_e2_val: if the property is found always valid by Value;
    • add_e2_wp: if the property is proved by WP;
    • add_e2_sc: if the property could have been removed as redundant by Scope (note: it could be necessary to keep this property anyway because it still might be useful for Value or WP computations);
    • add_e2_rv: if the property has been manually reviewed.

These naming conventions might seem to be quite cumbersome to use (especially the verification method suffix). However, as mentioned before, they make the automatic generation/verification possible, so they are highly recommended.