InvGend Frontend

InvGen Frontend

This tool can translate limited C input into InvGen input format.

Download Frontend(X86 Linux)
Download Frontend(X86 Windows)

Arguments

./frontend [-main fun-name] [-o out-file-name] [-domain number] input-file

The abstract interpreter InterProc is embedded in the frontend. Domain option selects the abstract domain to be used in the interproc.

-damain number	Abstract domains*
1	[Box;Octagon]
2	[Box;Octagon;PplPolyLoose]
3	[Box;Octagon;PolkaLoose]
4	[Box;Octagon;PplPolyStrict]

*Please look into InterProc documentation for meaning of abstract domains. InterProc is executed for each abstract domain which appears in the list for the given parameter to the option domain.

C-Input limitations

This tool can process only one function in the input file which shouldn't contain any function calls, array and pointers. It is only designed to supply experimental output to InvGen. Following are the examples which can be passed to frontend: simple.c, disj_simple.c, list.c, and confuse.c

Modeling non-deterministic choices using special variable NONDET.

  int NONDET;
  if(NONDET){
     ... 
  }

NONDET has to be declared as variables such that input comply with C-language.

Template specification in C

Each loop head in C program is a potential cut point for InvGen. One can declare template for each loop head separately by placing a call to function templ, just after the loop head, with a string as parameter. Following are the example to demonstrate the syntax for the parameter string:

Syntax	Shape
templ("2");	(a/\b)
templ("(2;2)");	(a/\b)\/(c/\d)
templ("(1;2)");	a \/ ( b/\c )
templ("[(1;1),1]");	( a\/b ) /\ c

InvGen Frontend

Arguments

C-Input limitations

Template specification in C

Bug Reports