tis-modifications Manual

Introduction

As said in Remove Alarms by Adding Annotations, the tis-modifications tool helps to track the source code modifications made on an application under analysis. The application is expected to be in a git repository, and the current version of the source files are compared to their version in an upstream branch. The idea is that all the modifications must be guarded by the macros presented below.

Macros

All the considered macros are named __TRUSTINSOFT_XXX__ where XXX is either one of the predefined name listed below, or a custom name specified using the --add option.

The predefined macros are:

  • __TRUSTINSOFT_HELPER__: for modifications to help the analysis such as unrolling loops, local slevel modification, using an intermediate variable (see Store Relational Information), etc.;
  • __TRUSTINSOFT_LABEL__: special case of __TRUSTINSOFT_HELPER__ where no comment is needed (see below). The labels are often used to add ACSL properties using the ACSLimporter plug-in (see Import ACSL Properties);
  • __TRUSTINSOFT_BUGFIX__: to fix a real problem in the code (patch);
  • __TRUSTINSOFT_TMPBUG__: for a workaround to avoid a (temporary) analyzer problem. In this case, it is a good idea to make a reference to the bug tracking system (JIRA) ticket if any.

All the ifdef guards (except the _TRUSTINSOFT_LABEL_ ones) are expected to be followed by a one line comment about the modification. The line is used in the --modif more explained below.

Example:

#ifdef __TRUSTINSOFT_HELPER__
  // declare and initialize intermediate variable
  int tmp = i + j;
#endif
  ...
#ifdef __TRUSTINSOFT_HELPER__
  // use intermediate variable
  //@ assert a_tmp: tmp == i + j;
  x = T[tmp];
#else
  x = T[i+j];
#endif

Modes

The tool has two main modes:

  • the diff mode shows the differences that are not protected by the macros listed above. So if all the modifications must be protected, this should always be empty.
  • the modif mode shows one line for each guarded modification with:
    • the source file name and line number,
    • the macro name,
    • the one line comment.

For instance:

src/compute.c:42 | _BUGFIX__ | // fix shift on negative value
src/utils.c:123  | _HELPER__ | // use intermediate variable
src/utils.c:456  | _LABEL__  | L:

Help message

The --help option gives more details about the available options:



This script helps to track the source code modifications made on an application
under analysis. The application is expected to be in a 'git' repository,
and the source files are compared to the original branch
(merge-base between HEAD and upstream branch).

All the modifications are supposed to be guarded by one of these macros:
- __TRUSTINSOFT_HELPER__:
  for modifications to help the analysis;
- __TRUSTINSOFT_LABEL__:
  special case of __TRUSTINSOFT_HELPER__ where no comment is needed (see below);
- __TRUSTINSOFT_BUGFIX__:
  to fix a real problem in the code (patch);
- __TRUSTINSOFT_TMPBUG__:
  for a workaround to avoid a (temporary) analyzer bug.
- or other __TRUSTINSOFT_XXX__ macros specified with the '--add XXX' option.

Moreover, each ifdef (except _TRUSTINSOFT_LABEL_) is supposed to be followed by
a one line comment about the modification.

Usage: ../binutils/tis-modifications/tis-modifications [<branch>] <-m|-d|-l|-r> [<other options>]
  where <branch> is the (optional) name of the upstream branch.
  Default: origin/master.

Options:
    -m | --modif    extract the list of the modifications
                    (source file, line number and one line comment)
    -d | --diff     show the differences that are not guarded
                    (should be empty)
    -l | --list-others show the list of the files, other than the *.[ch] files,
                    that have been added/deleted/modified
                    (should be only in TIS directories)
    -v | --verbose  in --diff mode, also print the filenames
    -a | --add <label> add the __TRUSTINSOFT_<label>__ to the processed macros
    -t | --top <dir> consider only the specified <dir> directory.
                    The default is to examine all the current git repository.
    -r | --ref      show the commit number of the reference
    -h | --help     show this help and exit