tis-aggregate Manual

Introduction

The purpose of the tis-aggregate tool is to collect and aggregate several results generated by TrustInSoft Analyzer.

To know how to use TrustInSoft Analyzer, refer to TrustInSoft Analyzer Manual. The Basic usage section below assumes that you already know how to build tis-analyzer command lines to run analyses and get Value analysis results as explained in Prepare the Analysis.

The next Advanced usage section presents more tis-aggregate commands and options.

Basic usage

Let’s first give an example of using tis-aggregate to get the coverage from several value analysis results. As explained in the Check the Coverage section of the TrustInSoft Analyzer Manual, the coverage measures the percentage of the code that has been reached by the value analyses, and it helps to detect dead code.

Let’s consider a small application composed of two source files and a header file:

File convert.c holding some library functions:
#include "convert.h"
int convert_atoi (char * arg, uint * p) {
  unsigned int x = 0;
  for (char* p = arg; *p != '\0'; p++) {
    char c = *p;
    if ('0' <= c && c <= '9')
      x = 10 * x + c - '0';
    else
      return 1;
  }
  *p = x;
  return 0;
}
static uint nb_digit (uint x, uint base) {
  if (x == 0)
    return 1;
  else {
    uint nb;
    for (nb = 0; x; x /= base) nb ++;
    return nb;
  }
}
char digit_name (int x) {
  return x < 10 ? '0' + x : 'a' + x - 10;
}
char * cv_to_base (uint x, uint base, char * buf) {
  if (buf && 2 <= base && base <= 16) {
    int nb = nb_digit (x, base);
    buf[nb--] = 0;
    while (nb >= 0) {
      int d = x%base;
      char c = d <= 9 ? '0' + d : digit_name (d);
      buf[nb--] = c;
      x /= base;
    }
  }
  else
    return NULL;
  return buf;
}
char * convert (char * str_x, char * str_base, char * buf) {
  unsigned int x, base;
  int err;
  err = convert_atoi (str_x, &x);
  if (err) return NULL;
  err = convert_atoi (str_base, &base);
  if (err) return NULL;
  return cv_to_base (x, base, buf);
}
char * cv_alloc (uint x, uint base) {
  uint n =  nb_digit (x, base);
  return malloc (n);
}
char * alloc_and_cv_to_base (uint x, uint base) {
  char * buf = cv_alloc (x, base);
  cv_to_base  (x, base, buf);
}
File convert.h that declares the library functions:
#include <stdio.h>
#include <stdlib.h>
#include <sys/types.h>

int convert_atoi (char * arg, uint * p);
char * convert (char * str_x, char * str_base, char * buf);
char * cv_to_base (uint x, uint base, char * buf);
/* Similar to [cv_to_base] but allocate a large enough buffer. */
char * alloc_and_cv_to_base (uint x, uint base);
File main.c holding the test entry point:

#include "convert.h"

int main (int argc, char * argv[]) {
  if (argc != 3) {
    printf ("Error: 2 arguments expects, got %d\n", argc);
    exit (EXIT_FAILURE);
  }

  char buf[100];
  char * x = argv[1];
  char * base = argv[2];
  char * p = convert (x, base, buf);

  if (p) {
    printf ("Result: convert %s in base %s = %s\n", x, base, p);
    return EXIT_SUCCESS;
  }
  else {
    printf ("Error: unable to convert %s in base %s\n", x, base);
    return EXIT_FAILURE;
  }
}

This application can for instance be analyzed with the following command line:

$ tis-analyzer -val -slevel 100 convert.c main.c -val-args ' 1234 10'

It gives results for the analysis of the application as if it were run with the two arguments 1234 and 10. Of course, it has to be run for other values to get more analysis results.

The Information about the Coverage section explains that the coverage is computed from csv files that are generated by tis-analyzer when using -info-csv-xxx options. The simplest way to generate those files is to just add the -info-csv-all option, and a name for the results, to the command line of each analysis.

For instance, to generate all the csv files in an existing results/ directory, the command line above becomes:

$ tis-analyzer -val -slevel 100 convert.c main.c -val-args ' 1234 10' \
  -info-csv-all results/test-1234-10

The argument of the option must be unique for each analysis since it is used as a base name to store the analysis result files. Those names are provided to tis-aggregate through what is called the INDEX file. Each line of this file holds the base name of one analysis results. The goal of the tis-aggregate tool is to collect the information from the analyses listed in this index file.

Before creating the index, let’s create another analysis with a different input:

$ tis-analyzer -val -slevel 100 convert.c main.c -val-args ' 1234 2' \
   -info-csv-all results/test-1234-2

So, the index file to create for these two analyses above would looks like:

Index file results/convert.aggreg.index
test-1234-10
test-1234-2

Now the coverage can be computed with:

$ tis-aggregate coverage results/convert.aggreg.index

It gives the following result:

Result of: tis-aggregate coverage results/convert.aggreg.index
File                                  MinStartLine  MaxEndLine  Function              MaxCyclomatic  #reached  #statements  Ratio  Comment
tests/tis-aggregate/main.c            41            41          __tis_globfini        1              2         2            100%   total
tests/tis-aggregate/convert.c         58            61          alloc_and_cv_to_base  1              0         5            0%     cannot be called at all
tests/tis-aggregate/convert.c         45            53          convert               3              7         11           64%    partial
tests/tis-aggregate/convert.c         6             17          convert_atoi          4              15        19           79%    partial
tests/tis-aggregate/convert.c         54            57          cv_alloc              1              0         3            0%     cannot be called
tests/tis-aggregate/convert.c         30            44          cv_to_base            6              24        30           80%    partial
tests/tis-aggregate/convert.c         27            29          digit_name            2              0         5            0%     may be called
tests/tis-aggregate/main.c            23            42          main                  3              10        15           67%    partial
tests/tis-aggregate/convert.c         18            26          nb_digit              3              12        14           86%    partial
TOTAL (functions)                                                                                    6         9            67%
TOTAL (all statements)                                                                               70        104          67%
TOTAL (stmts in reachable functions)                                                                 70        91           77%

It shows the list of the functions with the number of reachable statements and the total number of statements.

The three last lines labeled TOTAL summarize the coverage:

  • functions: number of analyzed functions over the number of functions.

  • statements: number of reachable statements over the number of statements.

  • stmts in reachable functions: number of reachable statements over the number of statements in the reachable functions.

We can for instance see that there are three unreachable functions:

  • alloc_and_cv_to_base is marked as cannot be called at all because there is no call to it in the program, and even its address is not used. So, there is no way to improve the coverage of this function without modifying the program.

  • Similarly, the cv_alloc is marked as cannot be called because there is a call to it, but only in a function that cannot be reachable. So, there is no way to improve its coverage either.

  • But the digit_name function is marked as may be called because there is a path to it from a reachable function, so its reachability may depend on input values. Indeed, it is not reached because it is only used for a base greater than 10.

So let’s run other analyses (with other inputs) and add them into the index file to enhance the coverage:

Index file results/convert2.aggreg.index
test-1234-10
test-1234-2
test-1234-16
test-0-10
test-a2b-10

The coverage becomes:

Result of: tis-aggregate coverage results/convert2.aggreg.index
File                                  MinStartLine  MaxEndLine  Function              MaxCyclomatic  #reached  #statements  Ratio  Comment
tests/tis-aggregate/main.c            41            41          __tis_globfini        1              2         2            100%   total
tests/tis-aggregate/convert.c         58            61          alloc_and_cv_to_base  1              0         5            0%     cannot be called at all
tests/tis-aggregate/convert.c         45            53          convert               3              9         11           82%    partial
tests/tis-aggregate/convert.c         6             17          convert_atoi          4              19        19           100%   total
tests/tis-aggregate/convert.c         54            57          cv_alloc              1              0         3            0%     cannot be called
tests/tis-aggregate/convert.c         30            44          cv_to_base            6              25        30           83%    partial
tests/tis-aggregate/convert.c         27            29          digit_name            2              4         5            80%    partial
tests/tis-aggregate/main.c            23            42          main                  3              13        15           87%    partial
tests/tis-aggregate/convert.c         18            26          nb_digit              3              14        14           100%   total
TOTAL (functions)                                                                                    7         9            78%
TOTAL (all statements)                                                                               86        104          83%
TOTAL (stmts in reachable functions)                                                                 86        96           90%

tis-aggregate coverage formats

To change the output format to csv (below) or html, the --format option can be used:

Result of: tis-aggregate coverage results/convert2.aggreg.index --format=csv
File,MinStartLine,MaxEndLine,Function,MaxCyclomatic,#reached,#statements,Ratio,Comment
main.c,43,43,__tis_globfini,1,2,2,100%,total
convert.c,58,61,alloc_and_cv_to_base,1,0,5,0%,cannot be called at all
convert.c,45,53,convert,3,9,11,82%,partial
convert.c,6,17,convert_atoi,4,19,19,100%,total
convert.c,54,57,cv_alloc,1,0,3,0%,cannot be called
convert.c,30,44,cv_to_base,6,25,30,83%,partial
convert.c,27,29,digit_name,2,4,5,80%,partial
main.c,25,44,main,3,13,15,87%,partial
convert.c,18,26,nb_digit,3,14,14,100%,total
TOTAL (functions),,,,,7,9,78%,
TOTAL (all statements),,,,,86,104,83%,
TOTAL (stmts in reachable functions),,,,,86,96,90%,

The csv format may be useful to be opened in a spreadsheet tool for easy selection of elements.

To know more about the other features of the coverage command, read the tis-aggregate coverage section below, or use:

$ tis-aggregate coverage --help

The tis-aggregate tool also provides other commands. The help command shows the available commands and the list of the options that are common to all of them:

$ tis-aggregate help

The following Advanced usage section presents some of them.

Advanced usage

tis-aggregate coverage

The Basic usage section above already explained how to use the coverage command, but some more details are given below.

Dead statements

To better understand the coverage, the dead code (i.e. the unreachable statements) needs to be analyzed. The easiest way to do that is to use the GUI, where the dead statements are highlighted in red, but it can be difficult to make a synthesis of the dead code over several analyses. So tis-aggregate can be used to generate the list of the statements that are not reached by any analysis.

With the --statements option, the list of the statements is filtered to keep only the unreachable statements. A path/base_statements.dead.xxxxxx.csv file (where xxxxxx is a random string) is generated. It holds information about these statements that are never reached by any analysis.

On the example below, it gives for instance:

Result of: tis-aggregate coverage results/convert2.aggreg.index --statements
File                                  MinStartLine  MaxEndLine             Function              MaxCyclomatic  #reached  #statements  Ratio  Comment
tests/tis-aggregate/main.c            41            41                     __tis_globfini        1              2         2            100%   total
tests/tis-aggregate/convert.c         58            61                     alloc_and_cv_to_base  1              0         5            0%     cannot be called at all
tests/tis-aggregate/convert.c         45            53                     convert               3              9         11           82%    partial
tests/tis-aggregate/convert.c         6             17                     convert_atoi          4              19        19           100%   total
tests/tis-aggregate/convert.c         54            57                     cv_alloc              1              0         3            0%     cannot be called
tests/tis-aggregate/convert.c         30            44                     cv_to_base            6              25        30           83%    partial
tests/tis-aggregate/convert.c         27            29                     digit_name            2              4         5            80%    partial
tests/tis-aggregate/main.c            23            42                     main                  3              13        15           87%    partial
tests/tis-aggregate/convert.c         18            26                     nb_digit              3              14        14           100%   total
TOTAL (functions)                                                                                               7         9            78%
TOTAL (all statements)                                                                                          86        104          83%
TOTAL (stmts in reachable functions)                                                                            86        96           90%
File                                   Line          Function               Number
tests/tis-aggregate/convert.c          28            digit_name             2
tests/tis-aggregate/convert.c          31            cv_to_base             24
tests/tis-aggregate/convert.c          31            cv_to_base             25
tests/tis-aggregate/convert.c          42            cv_to_base             26
tests/tis-aggregate/convert.c          42            cv_to_base             27
tests/tis-aggregate/convert.c          42            cv_to_base             28
tests/tis-aggregate/convert.c          51            convert                7
tests/tis-aggregate/convert.c          51            convert                8
tests/tis-aggregate/convert.c          55            cv_alloc               1
tests/tis-aggregate/convert.c          56            cv_alloc               2
tests/tis-aggregate/convert.c          56            cv_alloc               3
tests/tis-aggregate/convert.c          59            alloc_and_cv_to_base   1
tests/tis-aggregate/convert.c          60            alloc_and_cv_to_base   2
tests/tis-aggregate/convert.c          61            alloc_and_cv_to_base   3
tests/tis-aggregate/convert.c          61            alloc_and_cv_to_base   4
tests/tis-aggregate/convert.c          61            alloc_and_cv_to_base   5
tests/tis-aggregate/main.c             25            main                   2
tests/tis-aggregate/main.c             26            main                   3

Modified condition/decision coverage

Beside the statement coverage, MC/DC can also be computed. To know what it is, refer to MC/DC (Modified Condition/Decision Coverage).

To evaluate MC/DC, the test_i_decisions.csv must have been computed for each test_i analysis (see the About the Decisions section in the Tis-info Manual).

For instance, let’s consider the following example:

int D;
void g (char a, char b, char c) {
  if ((a != '0' || b != '0' ) && c != '0' )
    D = 1;
  else
    D = 0;
}
int main (int argc, char * argv[]) {
  // Skip input validation for a simpler example
  char * input = argv[1];
  g (input[0], input [1], input[2]);
}

When running an analysis with "000" as input:

$ tis-analyzer test.c --interpreter -mcdc -whole-program-graph -val-args " 000" -info-csv-all t_000
$ cat t_000_decisions.csv
File, Line, Function, #conditions, Conditions, Mixed, #ok(branches), #ok(mcdc), Traces
../test.c, 18, g, 3, 1+3+5, mixed, -1, -1, /0+0+X

We can see that there is only one decision, which is a mixed one. Since, the test calls g only once, there is only one trace in the results, and it leads to the else branch. The #ok column are meaningless here because the -mcdc-compute is not used since we want to do the computation using the results from several analyses.

Let’s run another analysis with "111" as input:

$ tis-analyzer test.c --interpreter -mcdc -whole-program-graph -val-args " 111" -info-csv-all t_111
$ cat t_111_decisions.csv
File, Line, Function, #conditions, Conditions, Mixed, #ok(branches), #ok(mcdc), Traces
../test.c, 18, g, 3, 1+3+5, mixed, -1, -1, 1+X+1/

Now, using tis-aggregate on these two analyses gives:

$ tis-aggregate coverage test1.aggreg --mcdc -o test1
$ cat test1.mcdc.csv | ../../tools/kit-tools/pp-csv-columns
File              Line  Function  Mixed  #conditions  #ok(branch)  Branch coverage  #ok(MC/DC)  MC/DC coverage  Details
../test.c         18    g         mixed  3            1            33.33%           1           33.33%          (ok; then branch dead; else branch dead)
TOTAL(decisions)                         1            0            0.00%            0           0.00%

The last TOTAL line shows:

  • the number of decisions,

  • the number of decisions with a 100% branch coverage,

  • the percentage of fully covered decisions in terms of branch coverage,

  • the number of decisions with a 100% MC/DC coverage,

  • the percentage of fully covered decisions in terms of MC/DC.

We can see that the branch coverage is not even reached with these tests.

Let’s add another one with "010" as input to have an 100% branch coverage:

$ tis-aggregate coverage test2.aggreg --mcdc -o test2
$ cat test2.mcdc.csv | ../../tools/kit-tools/pp-csv-columns
File              Line  Function  Mixed  #conditions  #ok(branch)  Branch coverage  #ok(MC/DC)  MC/DC coverage  Details
../test.c         18    g         mixed  3            3            100.00%          1           33.33%          (ok; MC/DC criteria not reached; MC/DC criteria not reached)
TOTAL(decisions)                         1            1            100.00%          0           0.00%

To get MC/DC, we still need to add a test with "011" as input as explained in MC/DC (Modified Condition/Decision Coverage):

$ tis-aggregate coverage test3.aggreg --mcdc -o test3
$ cat test3.mcdc.csv | ../../tools/kit-tools/pp-csv-columns
File              Line  Function  Mixed  #conditions  #ok(branch)  Branch coverage  #ok(MC/DC)  MC/DC coverage  Details
../test.c         18    g         mixed  3            3            100.00%          3           100.00%         (ok; ok; ok)
TOTAL(decisions)                         1            1            100.00%          1           100.00%

Now, the MC/DC requirements are fully reached.

Filters

Some options are provided to decide which functions should appear in the coverage results.

For instance, the coverage of the libc functions is usually not interesting to have, so the default is to ignore them, but they can be included when the --libc option is set.

The default behavior is to show the unreachable functions, but they can be skipped by setting the --skip-unreachable-fun option. It is especially useful when using the --libc option.

This is for instance the coverage computed on the first results/convert.aggreg.index index file shown above, without the unreachable functions:

Result of: tis-aggregate coverage results/convert.aggreg.index --skip-unreachable-fun
File                                  MinStartLine  MaxEndLine  Function        MaxCyclomatic  #reached  #statements  Ratio  Comment
tests/tis-aggregate/main.c            41            41          __tis_globfini  1              2         2            100%   total
tests/tis-aggregate/convert.c         45            53          convert         3              7         11           64%    partial
tests/tis-aggregate/convert.c         6             17          convert_atoi    4              15        19           79%    partial
tests/tis-aggregate/convert.c         30            44          cv_to_base      6              24        30           80%    partial
tests/tis-aggregate/main.c            23            42          main            3              10        15           67%    partial
tests/tis-aggregate/convert.c         18            26          nb_digit        3              12        14           86%    partial
TOTAL (functions)                                                                              6         6            100%
TOTAL (all statements)                                                                         70        91           77%
TOTAL (stmts in reachable functions)                                                           70        91           77%

Notice that the function coverage is now 100% since the unreachable functions are filtered out, but it might not always been the case when using the -val-use-spec option for instance.

The --skip-path, --skip-file and --skip-function options take a regular expression and specify the files or functions that should be skipped in the results. For example:

Result of: tis-aggregate coverage results/convert.aggreg.index --skip-function main
File                                  MinStartLine  MaxEndLine  Function              MaxCyclomatic  #reached  #statements  Ratio  Comment
tests/tis-aggregate/main.c            41            41          __tis_globfini        1              2         2            100%   total
tests/tis-aggregate/convert.c         58            61          alloc_and_cv_to_base  1              0         5            0%     cannot be called at all
tests/tis-aggregate/convert.c         45            53          convert               3              7         11           64%    partial
tests/tis-aggregate/convert.c         6             17          convert_atoi          4              15        19           79%    partial
tests/tis-aggregate/convert.c         54            57          cv_alloc              1              0         3            0%     cannot be called
tests/tis-aggregate/convert.c         30            44          cv_to_base            6              24        30           80%    partial
tests/tis-aggregate/convert.c         27            29          digit_name            2              0         5            0%     may be called
tests/tis-aggregate/convert.c         18            26          nb_digit              3              12        14           86%    partial
TOTAL (functions)                                                                                    5         8            62%
TOTAL (all statements)                                                                               60        89           67%
TOTAL (stmts in reachable functions)                                                                 60        76           79%

The --skip-file option may be used to exclude all the functions that come from some files. For instance:

--skip-file '^lib'

The --skip-path option may be used to exclude all the functions that come from some files in a specified directory, and may also include the file name prefix. For instance:

--skip-path some/path/ --skip-path another/path/xxx_

Advice about the source code

Warning

Because the coverage rely on the statement number inside the function, it is relevant only for the functions that have exactly the same statements in all the analyses, which means that, if different preprocessing options are used, they must not change that function source code.

However, some analyses may hold only part of the source code: the statements of the functions that are not in some analyses results are considered as if they were present but dead.

Despite the warning above, if some functions really need a different code for some analyses, one should follow the advice presented below to nonetheless get usable coverage results.

Conditional statements

When adding a conditional statement, a #else part with the same number of statements should be added so that the other statements of the function keep the same number across the analyses. For instance:

#ifdef TEST_1
  tis_variable_split (&x, sizeof(x), 10);
# else
  ;
#endif
  <statement>
Two versions of the same function

It is sometimes the case when two versions of the same function are needed for some analyses. In this case, instead of redefining the function like this:

#ifdef CONFIG_1
int f (...) {
  <code 1>
}
#else
int f (...) {
  <code 2>
}
#endif

It is better to define two functions to make them visible in all the analyses. The conditional code is only used to call one or the other:

int f_config_1 (...) {
  <code 1>
}
int f_other_config (...) {
  <code 2>
}
int f (void) {
#ifdef CONFIG_1
  return f_config_1 (...);
#else
  return f_other_config (...);
#endif
}

Adding Justifications

Optionally, the --justif option can be used to provide a file with some justifications for partially covered functions.

Each line of this file must be formatted as:

function_name, number of justified dead statements, justification

The free text in justification can be anything, but cannot contain a newline nor a comma (in order to produce a well-formed CSV file).

This file is useful when doing the verification several times to check whether the number of unreachable statements has changed since the last time the results have been reviewed.

For instance, for the example presented above, the justification file may look like:

File convert.justif holding some dead code justification:
main, 2, no test with wrong number of arguments.
convert, 2, no test with invalid char in second input.
digit_name, 1, always called with `x>=10`.

And then the coverage result becomes:

Result of: tis-aggregate coverage results/convert.aggreg.index --justif convert.justif
File                                  MinStartLine  MaxEndLine  Function              MaxCyclomatic  #reached  #statements  Ratio  #justified  Ratio  Comment
tests/tis-aggregate/main.c            41            41          __tis_globfini        1              2         2            100%   0           100%   total
tests/tis-aggregate/convert.c         58            61          alloc_and_cv_to_base  1              0         5            0%     5           100%   cannot be called at all
tests/tis-aggregate/convert.c         45            53          convert               3              9         11           82%    2           100%   no test with invalid char in second input.
tests/tis-aggregate/convert.c         6             17          convert_atoi          4              19        19           100%   0           100%   total
tests/tis-aggregate/convert.c         54            57          cv_alloc              1              0         3            0%     3           100%   cannot be called
tests/tis-aggregate/convert.c         30            44          cv_to_base            6              25        30           83%    0           83%    partial
tests/tis-aggregate/convert.c         27            29          digit_name            2              4         5            80%    1           100%   always called with `x>=10`.
tests/tis-aggregate/main.c            23            42          main                  3              13        15           87%    2           100%   no test with wrong number of arguments.
tests/tis-aggregate/convert.c         18            26          nb_digit              3              14        14           100%   0           100%   total
TOTAL (functions)                                                                                    7         9            78%    2           100%
TOTAL (all statements)                                                                               86        104          83%    13          95%
TOTAL (stmts in reachable functions)                                                                 86        96           90%    5           95%

tis-aggregate property-status

Beside the Prepare the Analysis that shows how to run tis-analyzer commands to get Value analysis results, the ACSL Properties section shows how to add some properties in the code to solve some problems, and how some of them can be proven using the WP plugin that involves theorem prover techniques (see Prove Annotations with WP).

As pointed out by the Conclusion of the TrustInSoft Analyzer Manual, all the results obtained by the analyses rely on hypotheses, and the code annotations are a large part of them. The property-status command helps to detect the annotations that are not verified by computing the status of each property across several analyses. To get an ok status, a property has:

  • either to be valid (or dead) in every value analysis results,

  • or to be proved by WP,

  • or to be said to be manually reviewed (see About property reviews).

Index

We have seen in Basic usage that the index file holds the list of the base names of the analyses results. The property-status command also needs to know where the results come from. So an optional second column has to be added to specify the kind of analysis that gave the results. It can be value, wp or other. A missing kind is equivalent to other. The property-status command only consider the value and wp results. So the index file may look like:

path_1/proj_1
path_2/proj_2, value
path_2/proj_3, wp
...
path_n/proj_n

Note

The paths are relative to the index file.

With the enhanced index file, the command may be run with:

$ tis-aggregate property-status appli.aggreg.index

To know more about the available property-status options, see the sections below or run:

$ tis-aggregate property-status --help

About property reviews

Some properties may be difficult to prove with the tools, so the user may prefer to justify them manually. The file holding the intellectual review must be a JSON file with a list of justifications, each one identifying the property and providing a textual justification. For instance:

Example of JSON file holding intellectual reviews:
[
  {
    "func": "get_index",
    "name": "@assigns",
    "justif": "this function just returns a number without modifying anything"
  },
  {
    "func": "main",
    "name": "sum_ok_rv",
    "justif": "since (i1<i2<50) then (i1+i2<100)"
  }
]

The file is provided to the tool with the --reviews option.

About property suffixes

Optionally, if the user follows the recommendations given in Naming the Annotations, i.e. takes care of adding a suffix to the property names, the --check-suffix option may be used to make the tool check if the computed status match the given suffix.

The default suffixes are:

  • _wp for properties that should be proved with WP (use the --wp-suffix to override it),

  • _val for properties that should be checked by the Value analysis (use the --val-suffix to override it),

  • _rv for properties that should be in the intellectual reviews (use the --review-suffix to override it),

  • the --ignore-suffix option can be used to specify a suffix to ignore, like _todo for instance.

Output

The default behavior of this command is to print the list of the properties that are not verified (according the criteria listed above). However, with the --all option, all the properties will be listed with information about their verification (and optionally information about the suffixes).

At the end of a study, it might be the case that some useless elements remain. For instance, if a property is valid in every analysis, it is useless to take some time proving it with WP. And if a property is valid in every analysis, or if it has been proved by WP, it is useless to keep a manual justification for it. When the --show-useless option is set, some warnings are generated for such useless elements and may help to clean the final results.

tis-aggregate sql-export

As seen in the tis-info Manual, the .csv files generated when using the -info-csv-all option can be used to explore the results of an analysis. But if you are familiar with SQL, it might be easier to use it to make more elaborated requests over several .csv files.

The sql-export command generate a sqlite database:

$ tis-aggregate sql-export appli.aggreg.index name

The appli.aggreg.index file is the index file as usual, and name is one of the analysis of the index. This second argument is needed because the database is generated only for one analysis at the moment.

Use the --help option to have for more information about this command, and to see examples.