Remove all parser.readLineDirectives = true usages

ispras · Oct 20, 2023 · ea85bc7 · ea85bc7
1 parent 3069de8
commit ea85bc7
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 10 deletions.
diff --git a/docs/klever_bridge.md b/docs/klever_bridge.md
@@ -64,13 +64,7 @@ sudo ./scripts/runner.py -c runner.json -d <path to Linux kernel>
 
 ## 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
@@ -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",