1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
Basic instructions
------------------
This is a very brief and preliminary description of the usage of source
code checkers and verifiers located in this directory. It is not intended
to be perfect since the formal verification is still work-in-progress, but
it should at least give you some basic hints.
If you want to try, say, the Clang static analyzer, follow the steps:
1. Go to the root directory of HelenOS source tree.
2. Run
make precheck
Configure the kernel according to your preferences. Remember that many
checkers have specific limitation on the target platform. They might
require the abstract platform abs32le or they might be suitable only
for platforms supported by some toolchain (e.g. ia32 and amd64 in the
case of Clang).
3. As HelenOS compiles, Jobfiles (e.g. kernel/kernel.job) are created.
4. Execute the checker while still in the source tree root directory. Do
not forget the argument "." which indicates the path to the source tree
root directory.
./tools/checkers/clang.py .
|