Uno Tool Synopsis



[Current Tool Version: 2.13 -- 26 October 2007]

See also static.html for an overview of currently available static analyzers.

Uno is a simple tool for source code analysis, written in 2001. It has two main goals:

Static analysis tools commonly suffer from a far too low signal-to-noise ratio: they tend to produce voluminous output that consists predominantly of false alarms: instances where the analyzer cannot determine the safety of the code and throws the problem back to the programmer. If any real defects are uncovered, they can be very hard to find in the long lists of pedantic or cosmetic issues.

Uno tries to be more specific, by concentrating exclusively on the three most commonly occuring, and most pernicious, defects in ANSI-C code. As a small example, below is the output from the traditional Unix tool lint, from its popular recent extension lclint, and the output from Uno for a trivial C program with a single major defect (a nil-pointer derefence):

Example 1:

$ num expr.c
 1 int *ptr;
 2
 3 void
 4 main(void)
 5 {
 6 	if (ptr)
 7 		*ptr = 0;
 8 	if (!ptr)
 9 		*ptr = 1;
10 }

$ lint expr.c
declared global, could be static
    ptr                 expr.c(1)

$ lclint expr.c
LCLint 2.5q --- 26 July 2000

expr.c:4:1: Function main declared to return void, should return int
  The function main does not match the expected type. (-maintype will suppress message)
expr.c: (in function main)
expr.c:9:4: Dereference of null pointer ptr: *ptr
  A possibly null pointer is dereferenced.  Value is either the result of a
  function which may return null (in which case, code should check it is not
  null), or a global, parameter or structure field declared with the null
  qualifier. (-nullderef will suppress message)
expr.c:1:6: Variable exported but not used outside expr: ptr
  A declaration is exported, but not used outside this module. Declaration can
  use static qualifier. (-exportlocal will suppress message)

Finished LCLint checking --- 3 code errors found

$ uno expr.c
uno: in fct main, possible global use of deref before def:
     statement  : expr.c:9: (*ptr)=1
     declaration: expr.c:1: int *ptr;
Note that lint misses the one significant error, and lclint hides the error report in a list of explanations and cosmetic complaints. (This may not look like much of a problem for a ten-line program, but it decidedly is when the code reaches a more typical size and the list of complaints starts running in the thousands.) Uno restricts itself to reporting the one thing that counts: the possibility of a core-dump on the execution of the statement on line 9. Note that the execution of the statement on line 7 would have a similar effect, but that statement is unreachable.

The tool can be run also in a picky mode, where it generates the more cosmetic complaints about fall-thru on case switches, externs that could be declared static, redundant declarations etc. By default these messages are suppressed.

Application Specific Properties

Uno derives most of its power from its ability to accept user-defined properties of application specific requirements, and then check the source code for strict compliance with these requirements.

To illustrate the process, two examples of user-defined Uno properties are shown below. One relatively small, and one sligthly larger.

Example 2:

Here is how a Uno property can be defined in about eight lines of C code to check for the occurrence of any side-effects or function calls in assert statements.

void
uno_check(void)                                 // check for side-effects in assertions
{
        if (select("assert", FCALL, NONE, 0))   // identify the statements of interest
        if (select("", DEF|FCALL, NONE, 0))     // in those, select symbols Defined and Fct Calls
        if (exclude("assert", ANY, NONE, 0))    // but exclude the symbol named assert
                error("side effect or fct call in assert");  // if anything remains, complain
}
Note that the property is defined in ANSI-C, using a small set of predefined primitives to access standard dataflow information that is collected by the Uno tool. Uno runs the check over all paths in the control flow graphs of all procedures in the source tree, and reports any violations it finds.

Example 3:

The following Uno property checks proper usage of memory allocation routines malloc and free.

void
uno_check(void)
{
	if (select("malloc", FCALL, NONE, 0))    // find all calls to malloc
	if (select("", DEF, NONE, 0))            // select symbols defined in call
	{	if (select(MATCH, DEF, NONE, 1)) // check if any were previously marked
			error("value allocated not freed"); // if so, complain
		else
			mark(1);                 // else mark the symbol
	}

	if (select("free", FCALL, NONE, 0))      // find all calls to free
	{	if (select("", USE, NONE, 0))    // select symbol used in call
		{	if (select(MATCH, DEF, NONE, 1))  //check if previously marked
				unmark();        // if so, remove the mark
			else                     // else complain
				error("freeing a symbol not previously malloced");
		} else
			error("no argument to free");
	}

	if (path_ends())                         // at any return or exit statement
	if (select("", ANY, NONE, 1))            // check if any frees are pending
	{	if (known_zero())                // if the value of the symbol is zero
			no_error();              // no problem, malloc probably returned null
		else                             // else the symbol should be freed
			error("malloc without free");
	}
}

Documentation

The papers, and a manual page, are included in the tar archive.

Source Code (Version 2.13 -- 26 October 2007)

uno_v213.tar.gz (tar archive, gzipped) can be compiled for PC or for Unix.
(Earlier version remain available -- change the tarfile name accordingly.)

Version 2.13 (26 Oct 07) Handles larger data arrays, and deals better with some quirks in lexer.l when compiled on a linux platform.

Version 2.12 (11 Aug 07) Handle 0LL, and empty initializer lists (courtesy Dany Vereertbrugghen, lucent). The tool will still complain if a structure is passed to a function without prior initialization. Fix pending.

Version 2.11 (2 March 07) Handle larger inputs. Better behavior on self-test. Removes problem with some preprocessors where uno could choke on an unexpected format for linenumber directives. Thanks to rainer from samhain labs.

Version 2.9-2.10 (Feb 06) Small fixes only. In pedantic mode, uno will now treat pointers that are initialized to zero as being uninitialized. This is annoying sometimes when you want to initialize the pointer to turn off a report from uno, but it is a little safer. Several patches courtesy of Jerry James.

Version 2.8 (Jun 05) Small fixes only.

Version 2.7 (May 05) New commandline option for uno_local: "-nova" will disable the redefinition of va_start, va_arg, and va_end, which sometimes causes preprocessor complaints. Bug fix in uno_global (didn't use a -a argument correctly in all contexts).

Version 2.6 (Apr 05) Uno now looks for the uno_suppress file in both the current directory and in the optional work directory that can be specified with a -W argument to uno or uno_local.

Version 2.5 (March 05) If conditionals followed by a null statement (as in "if (c);" ) are now only reported with "uno_local -picky" (or equivalently with "uno -w" which calls uno_local with the picky flag as well).
Uno_local now accepts an optional file called "uno_suppress", placed in the directory where uno is invoked, that can contain an arbitrary number of lines with two fields per line, separated by a single tabspace. The first field gives a filename, and the second field gives a line number in that file. No error reports will be printed for the lines listed in this file. For an example see the file src/uno_suppress. Of course, ideally you want to generate this file mechanically from the sources, by looking for comment tags that the user inserts (linenumbers change when code is edited).
A script called "mk_uno_suppress" is provided, which looks for comments of the form: /* @uno_suppress -- comment */ and creates the uno_suppress file automatically when run (Unix system assumed - requires grep and sed commands).

Version 2.4 (Jan 05) PARAM tags now stick, and appear in all uses of a symbol. some more small bug fixes, added some more tags in dtags.h to make it easier to track things in properties. added some more example properties in the prop/ subdirectory. added a webpage fsm.html, with information on the basic method of building state machines as uno properties, linked from the uno main webpage. added a new option to uno_local (-fullpaths) to force the printing of complete path information for all property violations (this used to be the default). the default is now to just give the line number of the violation -- unless -fullpaths is specified on the uno_local command line. not supported via the basic uno interface (which call uno_local with default arguments in the background).

Version 2.3 (Dec 04) better directory structure; fixed parser to conform better to expectations of different versions of bison. (the version number in this copy of the tar archive is accidentily still numbered 2.2).

Version 2.2 (Nof 04) big cleanup off the code, making the code more portable and leading to a much smaller tar file with the same functionality.

Version 2.1 (Aug 04) fewer bugs, prefixing a variable name with 'unused' now tells uno that the variable is intentially not used. Thanks to Jerry James (University of Kansas) for several improvements.

Version 2.0 (Jul 04) bug fixes, increased precision, more stable version.

Version 1.8 (Oct 03) better treatment of function pointers, though not perfect.

Version 1.7 (Oct 04) global analysis did not interpret 'exit()' correctly; other small fixes.

Version 1.6 m(May 03) inor bug fixes.

Version 1.5 (Apr 03) fixes a glitch in global pointer derefencing detection (would detect *p = x, but not x = *p, if p is global pointer without explicit initialization).

Version 1.4 (Apr 03) fixes a glitch in array bounds analysis, which would fail to catch very simple bounds violations.

Version 1.3 (Apr 03) fixes the problem fixed in version 1.2 better (...), so that it still works on Unix systems too. Without this fix, global analysis can dump core on Unix systems.

Version 1.2 (Feb 03) fixes a problem with the parsing of fct_call() primitives from uno_check properties. (Reported by Radek Vingralek.)

Version 1.1 (Feb 03) fixes a problem in version 1.0 where support for user-defined local properties was not working correctly. It also adds a library of sample uno_check properties in directory Prop.

Contact Information

For more information contact gerard [insert atsign here] spinroot.com.

See also http://www.spinroot.com/static/ for an overview of static source code analyzers for C.


Page last updated 11 August 2007