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.