Tutorials

Under construction.

All stanse command lines presented here may contain -g switch which will run GUI with the configuration set on the line. Error are then easily traceable in the GUI.

Running Stanse

The following example will check my_file.c by the 3 defined checkers:

java -jar stanse.jar -c AutomatonChecker:first_checker_def.xml \
	-c AutomatonChecker:second_checker_def.xml \
	-c ThreadChecker:third_checker_def.xml \
	my_file.c
      

The file needs to be preprocessed or must not depend on any magic compiler flags like -I -D etc. This is mostly not what one wants. Other methods exist (stcc, makefile and jobfile support, see below).

Incorporating compiler flags

This can be easily achieved file-by-file:

rm -f /tmp/stanse_job
JOB_FILE=/tmp/stanse_job stcc file1.c -o file1.o -DIMPORTANT_DEFINE \
	-I /usr/include/my_path/ -Wall -O2 -c
JOB_FILE=/tmp/stanse_job stcc file2.c -o file2.o -DIMPORTANT_DEFINE \
	-I /usr/include/my_path/ -Wall -O2 -c
:
:
java -jar stanse.jar -c AutomatonChecker:<path>/kernel_memory.xml \
	--jobfile /tmp/stanse_job
      

Checking an external kernel module

This will check a kernel module in my_module directory:

java -jar stanse.jar -c AutomatonChecker:<path>/kernel_memory.xml \
	--makefile my_module/Makefile
      

Note that the directory has to be cleaned by make, because Stanse will run make. In case it wasn't, nothing would be checked, because make would shout 'nothing to be done'.

Checking whole kernel

Configure kernel as usual and then run:

rm -f /tmp/stanse_job
JOB_FILE=/tmp/stanse_job make CC=stcc all
java -jar stanse.jar -c AutomatonChecker:<path>/kernel_memory.xml \
	--jobfile /tmp/stanse_job
      

Or any other kernel makefile target such as drivers/, bzImage, etc.

Even kernel modules from the previous point may be checked this way.

Exporting errors

Stanse supports an errors export to an XML file. The switch --stats-build output.xml will store the errors into output.xml. It can be later investigated using --stats-err-guitracing output.xml:/dev/null.