Static analysis for AVR code with Splint

Over on #avr, static analysis came up, particularly, getting Splint to run. _abc_ put this guide together, which I’ve reproduced verbatim below.

Running splint(1) on avr-gcc source code


Version 0.0 - tested 15.05.2012

by _abc_ @irc.freenode.org

software versions:
splint 3.1.2 compiled from source
avr-gcc-4.5.1 as supplied by Atmel (binary build for Linux)

Splint is a static C source code analyzer which can help
keep C source files and headers tidy and consistent. It can
also prevent a lot of silly errors, which is more important
in embedded C code than elsewhere. Many embedded code error
signals involve smoke, sparks, and lost devices.

Splint was never designed to run on embedded C, with its
extensions. In addition to that, splint has not been maintained
that much. The Wikipedia article on splint mentions that is is
'not relevant' as software anymore and that its Wikipedia page
should be removed. I disagree with that statement.

The following shows how splint (3.1.2) can be run successfully
on abr-gcc source code in 2012.

Checklist:

1. Install splint (it compiles cleanly from source on any gnu
compiler equipped system, using ./configure && make && sudo
make install). Alternately, get the distribution specific
package of splint if it exists.

2. Make a copy of your embedded source files for backup in case
something goes wrong.

3. Get used to the fact that the splint manual page is not so
useful. Running splint -help [something] 2>&1|less is much more
so. The pdf manual which comes in the package of splint 3.1.2 is
dated 2003 (proudly, on the first page). That's okay, since the
C standard most used today is dated 1999 (C99)...

4. Copy the following commands into a shell command file in
your project directory, and edit the relevant parts (path to
avr installed toolchain include, source file name etc):

--snip--
#
# splint-avr-gcc-code.sh 644
#
# V0.0 tested 15.05.2012 by _abc_ @ irc.freenode.org
#
# run the splint static source analyzer on a avr-gcc C source code file,
# in a avr-gcc compatible way.
#
# initial revision, tested with avr-gcc, throws lots of warnings on avr-gcc
# includes but runs AS LONG AS:
# i. __fuses and __lockbits sections are hidden from splint using 
#    #ifndef S_SPLINT_S
#      ...
#    #endif
# ii. any binary constants (0b000f) in the C source are either rewritten as
#   decimal or hex numbers, OR their sections are guarded as above, and
#   binary or hex values are provided instead.
#
# Comment: the splint parser should be patched to accept binary constants.
# The usual makefile used for project building should have a new section
# (target) called lint or splint which should lint the source. It can be
# easily written by adding the code below:
#

## adjust to suit your installation
AVR_TOOLCHAIN_INSTALLED_LOCATION="/some/where/" ;# edit me

SRC="mysource.c" ;# edit me, ONE source file per shell file for now

DEFS="-D__AVR_ATmega8__" ;# etc, edit this

#SPLINT_EXTRA_ARGS="-nolib"
## actually run
splint \
	-preproc \
	-unrecogcomments \
	$SPLINT_EXTRA_ARGS \
	-I${AVR_TOOLCHAIN_INSTALLED_LOCATION}/avr/include/ \
	$SRC
--snap--

5. while editing the required areas of the command file above, also 
read its header. It explains how the source can be splint proofed. It is
really easy. The -unrecogcomments comment is needed because there are
some semantic comments in the header files which throw errors. The other
ways to splint proof your code are explained by executing the commands:

  splint -help parseerrors 2>&1|less

in a shell.

6. splint should really be updated with embedded C extensions, especially
the 0b0001 style binary constant support.

7. avr-libc maintainers should run splint as above on sources which include
them (hello_world.c with just #include  and #include  are
enough for a start), as splint shows more than 90 warnings on running through
the avr-libc headers included by the simple main alluded to above at the
time of this writing.

-- the end --

Note, I haven’t actually used splint myself, on AVR code or regular desktop code. I do however endorse static analysis, having used PMD and friends on java code quite a lot. If you don’t like splint, or are looking for alternatives, perhaps something still being maintained, abcminiuser suggests Cppcheck, which covers both C and C++. There’s also the commercial Coverity and gimpel. I’ve not used any of these, but it seemed like such a worthwhile record that I was loathe to lose the discussion the depths of IRC logs.

Leave a Comment

NOTE - You can use these HTML tags and attributes:
<a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>