~martin-decky/helenos/rcu

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 .