.ds U U\s-2NO\s0.TH UNO 1.CT 1 program_analysis nil_pointers.SH NAMEuno \(mi static analysis tool for ANSI-C programs.SH SYNOPSIS.B uno.BI "[-D...] [-U...] [-I...] [-CPP=...] [-a] [-g x] [-h] [-l] [-m x] [-n] [-p x] [-s] [-t] [-u] [-V] [-v] [-w] [-x f] \f1*.c".SH DESCRIPTION\*U is a tool for analyzing programs written in ANSI-C.By default, the tool scans the sources for the threemost commonly occuring defects of C programs:use of \f2u\f1ninitialized variables, \f2n\f1il-pointerdereferencing problems, and \f2o\f1ut-of-bound arrayindexing problems. It can optionally also report on aseries of other, more cosmetic, flaws of the code, suchas redundant variable and function declarations, unusedfields in structures, variables set but not used, theuse of conditions with side-effects, etc..PPThe \*U analysis proceeds in two phases: a local analysisof each function in the code, and a global analysis for theentire program. The local analysis can be done on alsoincomplete code, but the global analysis expects a completeprogram that can be searched starting from the \f2main()\f1routine..PP\*U allows the user to define new propertiesto check for, by writing simple C-functions thatencode the required check. The properties canspecify either a local check, applied to each functionseparately, or a global check, applied to the programas a whole.  The local check applies to the use oflocal variables of any type, the global check appliesto the use of global pointers only..PPThe first group of options allows for the definition ofcompiler directives on the command line, to guide thepreprocessing of the sources..TP.B "-Dname=def"Define.B namewith value.B defas if by a \f2#define\f1..TP.B "-Dname"Define.B namewith value 1..TP.B "-Idir"Add directory.B dirto the list of directories that is searched by the preprocessorfor include files..TP.B "-Uname"Remove any definitions of name, where name is areserved symbol that may be predefined by the preprocessor.If present, this action supersedes the possible use of .B "-D"for the same symbol, irrespective of the order in whichthese options are given..TP.B "-CPP=..."Set the preprocessor to the name specified. For instance,\fBCPP="cl -EP -nologo"\f1..PPThe next set of options controls how the analysis is performed..TP.B -aReport all error paths in the local analyses, rather than only pathsthat end in distinct statements in the source..TP.B "-g x"Check the \f2global\f1 property definition stored in file \f2x\f1,instead of the default property for the use or dereferencingof uninitialized global pointers (by default initialized to zero).By convention, the property function must bedeclared as \f2void uno_check(void) {}\f1..TP.B -hor.B -helpPrints a usage summary with the main tool options..TP.B -lPerform only the local analysis, do not write intermediate files..TP.B "-m f"Use a master definitions file, with \*U type definitions, for thelocal analyses. This can be useful in cases where the sourcebeing analyzed is incomplete, e.g., header files are missing.The user can add terse declarations of symbol names that shouldbe understood to be typenames by the \*U parser.By convention this is done in a file named \f3_uno_.dfn\f1, which isplaced in the same directory where \*U is invoked. The filemay contains entries of the form:.DSUnoType bool;UnoType complex;.DE.IPwhich suffice to identify them as typenames to the tool, withoutrequiring further detail.Definitions are given one per line, and terminated by a semi-colon.The file may also contain any standard preprocessing commandunderstood by ANSI-compliant C preprocessors. This can be used toavoid the expansion of macro names, for instance, so that theycan be tracked in \*U properties, e.g.:.DS#define assert(x)	Assert(x)	/* avoid macro-expansion */.DE.IPIf the filename for the definitions file is \f3_uno_.dfn\f1, andthe file is placed in the directory where \*U is invoked, thedefinitions file will automatically be included.If the file name is different, or located elsewhere, the \f3-m\f1option can be used..TP.B -nIgnore all preprocessing directives in the source files being analyzed.This can be useful for analyzing output from a preprocessor, where thedirectives can be non-ANSI compliant. Cross-referencing information tothe original source files is lost in this case..TP.B "-p x"Check the \f2local\f1 property definition stored in file \f2x\f1.As with global checks, the property function must bedeclared as \f2void uno_check(void) {}\f1..TP.B -sPrint only the symbol table information for each source file, and exit..TP.B -tProvide detailed function call traces for any error scenariofound during the global analysis..TP.B -uComplain about redundancies of all sorts..TP.B -VPrint the current \*U version number and exit..TP.B -vVerbose mode, currently mostly for debugging purposes..TP.B -wPicky, or lint-like, mode.Complains about a larger variety of things, including morecosmetic flaws in the code. Includes.B -uand.B -l ..TP.B "-x f"Declare f to be a function that does not return. This affectsthe control-flow of the program and can therefore be importantfor the results of the analysis.  By default, only the functionsnamed.I exit ,.I fatal ,and.I panicare presumed not to return control to the caller..SH NOTESUnless the.BI -lflag is used, \*U writes a small intermediate fileat the end of the local analysis for each source file.The intermediate files for all source filesenables the global analysis.Each intermediate file has the same base-name asthe \f2.c\f1 source file from which it was generated,but with the extension \f2.uno\f1 instead of \f2.c\f1.\*U cleans up the intermediate files at the end ofthe global analysis. For very large source trees itcan be beneficial to preserve the \f2.uno\f1 files inbetween subsequent analysis, so that they are onlyrecreated when necessary..SH SEE ALSOMore background information on the design of the tool,examples of properties and applications, can be found in:.br.in +2G.J. Holzmann, `\*U: Static Source Code Checking for User-Defined Properties,'.br\f2Proc. IDPT 2002\f1, 6th World Conf. on Integrated Design & Process Technology,June 2002, Pasadena, CA..in -2.br