Merge pull request #5583 from tautschnig/use-jq

Use jq for checking JSON syntax

Author: tautschnig

regression/solver-hardness/CMakeLists.txt

@@ -1,2 +1,8 @@
-add_test_pl_tests(
-  "../chain.sh $<TARGET_FILE:cbmc>")
+find_program(JQ jq)
+if(NOT JQ)
+  message("Skipping solver-hardness tests: couldn't find jq in your path")
+else()
+  add_test_pl_tests(
+    "../chain.sh $<TARGET_FILE:cbmc>")
+endif()
+

regression/solver-hardness/Makefile

@@ -6,10 +6,13 @@ include ../../src/common
 CBMC_EXE=../../../src/cbmc/cbmc
 
 test:
+ifeq (, $(shell which jq))
+	echo "solver-hardness tests skipped (can't find 'jq' in your path)"
+else
 	@../test.pl -e -p -c "../chain.sh $(CBMC_EXE)"
+endif
 
-tests.log: ../test.pl
-	@../test.pl -e -p -c "../chain.sh $(CBMC_EXE)"
+tests.log: ../test.pl test
 
 show:
 	@for dir in *; do \

regression/solver-hardness/chain.sh

@@ -7,5 +7,5 @@ args=${*:2:$#-2}
 
 $cbmc ${name} ${args}
 CBMC_RETURN_CODE="$?"
-../parse_json.py "solver_hardness.json"
+jq -c . "solver_hardness.json"
 exit ${CBMC_RETURN_CODE}

regression/solver-hardness/parse_json.py

@@ -5,7 +5,6 @@ main.c
 ^SIGNAL=0$
 ^\[main.assertion.\d+\] line \d+ assertion a \+ b \< 10: FAILURE$
 ^VERIFICATION FAILED$
-^Valid JSON File$
-\"SAT_hardness\": \{(\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+)\}
+\"SAT_hardness\":\{(\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+)\}
 --
 ^warning: ignoring