Caution
The tis-mk-main
tool is not available in this version.
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.
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>
tis-main-dummy.c
);-prog-name <name>
argv[0]
(default is UNKNOWN
);-main <function-name>
tis_main
);-f
-with-env
char** env
;-help
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>
-tis-cst <size>
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);
}
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.