Klever

Regarding rule specifications and their base we just kept in mind an ability to verify C programs in addition to Linux kernel loadable modules. Since Klever 2.0 this ability should be supported that requires some changes. Among others they are:

• Place rule specifications (they include all other specifications) into top-level directory specifications. Move file rule specs.json there and rename it to base.json.
• Move files ldv-test.* from the top-level directory of the main verification job to appropriate place (likely to several jobs which need this).
• Move generic:memory to linux:memory safety. The corresponding rule specification does too Linux specific and it can not be used for anything else.
• Ditto move sync:race to linux:concurrency safety.
• Move out all Linux specifics from verifier/*. Partially this was already done by Alexey Polushkin, but this breaks Linux stuff.
• Get rid of two redundant parameters from job.json, namely rule specifications DB and verifier profiles DB.
• Rename parameter rule specifications to requirements.
• Support a requirements tree within former rule specifications.json to arrange them nicely, e.g.:
  

      "linux": {
        "decsription": "...", # Common description for all underlying requirements.
        "template": "...", # Common template for all underlying requirements.
        ...
        "concurrency safety": {...},
        ...
        "kernel": {
          ...
          "locking": {
            "mutex": {...},
            "rwlock": {...},
            "spinlock": {...}
          },
          ...
        },
        ...
        "memory safety": {...},
        ...
      }
  

• Fix everything that rely upon changed things, e.g. environment model specifications, preset marks, tests and of course scripts.

If somebody has some notes, it is better to say them ASAP as starting from tomorrow everything mentioned will be implemented.