From ea85bc73a60482bc959295eb80c8b66c61d19131 Mon Sep 17 00:00:00 2001 From: Mordan Vitalii Date: Fri, 20 Oct 2023 20:16:13 +0530 Subject: [PATCH] Remove all parser.readLineDirectives = true usages --- docs/klever_bridge.md | 10 +--------- properties/properties.json | 2 +- 2 files changed, 2 insertions(+), 10 deletions(-) diff --git a/docs/klever_bridge.md b/docs/klever_bridge.md index 57d4d7a..78e7677 100644 --- a/docs/klever_bridge.md +++ b/docs/klever_bridge.md @@ -64,13 +64,7 @@ sudo ./scripts/runner.py -c runner.json -d ## Klever config -In order to visualize error traces CPAchecker config must include the following: -```json -{"-setprop": "parser.readLineDirectives=true"} -``` -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 +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: @@ -79,5 +73,3 @@ If you need to visualise correctness witnesses in CV, the following options are {"-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. diff --git a/properties/properties.json b/properties/properties.json index 55f57b6..ee062f6 100755 --- a/properties/properties.json +++ b/properties/properties.json @@ -22,7 +22,7 @@ "-skipRecursion": [], "-stack": ["10m"], "-setprop": [ - "parser.readLineDirectives=true", + "parser.readLineDirectives=false", "output.disable=true", "cpa.predicate.abortOnLargeArrays=false", "cpa.arg.proofWitness=witness.correctness.graphml",