tis-mk-main Manual¶

Description¶

The tis-mk-main tool generates a C file containing a new entry point for a program expecting command line arguments. More precisely, the generated file contains a function tis_main calling the main function of the original program with the specified arguments.

How to use it¶

The command line to call the tool is composed of two parts separated by a double dash -- and so it looks like:

$ tis-mk-main <options> -- <arguments>

The options to change the default behavior are:

-o <file>

name of output file (default is tis-main-dummy.c);

-prog-name <name>

name of the original program used as argv[0] (default is UNKNOWN);

-main <function-name>

name of the main function to generate (default is tis_main);

-f

forces overriding if the output file already exists;

-with-env

generates a third argument for new main function : char** env;

-help

prints a help message.

The arguments can be listed as they would be in the command line to call the original program. Arguments beginning by a - have to be preceded by a - alone (see example below). Two more options are provided to specify some indeterminate arguments:

-tis-var <size>

generates indeterminate string argument of length between 0 and n;

-tis-cst <size>

generates indeterminate string argument of length n.

Example¶

For instance, following command generates a function my_main in a file new.c that calls the main function of the application to analyze with 3 arguments:

$ tis-mk-main -f -main my_main -o new.c -prog-name PROG
            -- arg1 -tis-var 2 - -opt1 -tis-cst 2 - --opt2

The generated file is:

#include "tis_builtin.h"

char* argv[6];

char argv_0[] = "PROG";
char argv_1[] = "arg1";
char argv_2[3];
char argv_3[] = "-opt1";
char argv_4[3];
char argv_5[] = "--opt2";

extern int main(int argc, char* argv[]);

void my_main() {
  tis_make_unknown(argv_2, 2);
  argv_2[2] = 0;
  if (tis_interval(0,1)) {;
    argv_4[0] = tis_char_interval(-0x7F,-1);
  } else {
    argv_4[0] = tis_char_interval(1,0x7F);
  }
  argv_4[2] = 0;
  if (tis_interval(0,1)) {;
    argv_4[1] = tis_char_interval(-0x7F,-1);
  } else {
    argv_4[1] = tis_char_interval(1,0x7F);
  }
  argv_4[2] = 0;
  argv[0] = argv_0;
  argv[1] = argv_1;
  argv[2] = argv_2;
  argv[3] = argv_3;
  argv[4] = argv_4;
  argv[5] = argv_5;
  main(6, argv);
}

Generate an Entry Point with CFP¶

Instead of using tis-mk-main, the Context From Precondition plug-in (CFP for short) can be used to generate an entry point from the preconditions of the function to analyze. This is useful when one wants to be sure that the analysis context is not smaller than the context specified by those preconditions (see Pre-conditions for more information).

To generate a context for a function f, the command line looks like that:

tis-analyzer <options and c files> -cfp -cfp-input f

For instance, the preconditions for f could be:

/*@ requires 0 <= size <= 100;
    requires \valid_read (in + (0..(size - 1)));
    requires \initialized (in + (0..(size - 1)));
    requires out == \null || \valid (out + (0..(size - 1)));
 */
int f (int * out, int const * in, int size);

In most cases, the files __fc_builtin.h and stdlib.h from the tool standard library are needed in order to make the CFP plug-in work correctly, so they should be included in the project.

Since CFP generates the code in a new project, the -then-last option must be used to switch to this project and be able to, for instance, run the value analysis on it:

tis-analyzer <options and c files> -cfp -cfp-input f -then-last -val

More CFP options are available, see the plug-in’s help (using the -cfp-help option) for more information.