tools/checkers/howto.txt

   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 .