As said in Remove Alarms by Adding Annotations,
tis-modifications tool helps to track the source code modifications
made on an application under analysis.
The application is expected to be in a
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
All the considered macros are named
XXX is either one of the predefined name listed below,
or a custom name specified using the
The predefined macros are:
for modifications to help the analysis such as unrolling loops,
using an intermediate variable (see Store Relational Information), etc.;
special case of
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);
to fix a real problem in the code (patch);
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.
ifdef guards (except the
are expected to be followed by a one line comment about the modification.
The line is used in the
--modif more explained below.
#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
The tool has two main modes:
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.
modif mode shows one line for each guarded modification
the source file name and line number,
the macro name,
the one line comment.
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 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: ../../tools/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