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