|
Last change
on this file was 96e7a94, checked in by Martin Decky <martin@…>, 15 years ago |
|
add simple HOWTO
|
-
Property mode
set to
100644
|
|
File size:
1.0 KB
|
| Line | |
|---|
| 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 .
|
|---|
Note:
See
TracBrowser
for help on using the repository browser.
