Skip to content

Commit

Permalink
Add more options in Klever bridge documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
vmordan committed Sep 7, 2023
1 parent 9ff63e4 commit 763c16e
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions docs/klever_bridge.md
Original file line number Diff line number Diff line change
Expand Up @@ -61,9 +61,14 @@ In order to visualize error traces CPAchecker config must include the following:
```
Note, Klever will not visualise traces with such option.

Also Klever job configuration should specify `Keep intermediate files inside the working directory of Klever Core` inside
`Other settings` section in order to visualize generated files in the error trace.

If you need to visualise correctness witnesses in CV, the following options are required:
```json
{"-setprop": "cpa.arg.proofWitness=witness.correctness.graphml"},
{"-setprop": "cpa.arg.export=true"},
{"-setprop": "cpa.arg.compressWitness=false"}
```

If you need to add coverage, set flag `Collect total code coverage` in the Klever job config.

0 comments on commit 763c16e

Please sign in to comment.