Skip to content

Commit 5f4c82d

Browse files
tautschnigtautschnig
authored
Merge pull request #8713 from tautschnig/goto-functions-json
Add support for reading GOTO functions from JSON
2 parents b0156a3 + 6d3ce5d commit 5f4c82d

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

42 files changed

+1773
-97
lines changed

‎doc/man/symtab2gb.1‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,9 @@ https://github.com/model-checking/kani).
1919
\fB\-\-out\fR \fIoutfile\fR
2020
Specify the filename of the resulting binary (default: a.out)
2121
.TP
22+
\fB\-\-goto\-functions\fR \fIfile\fR
23+
Specify a file containing JSON-encoded goto functions
24+
.TP
2225
\fB\-\-verbosity\fR #
2326
verbosity level
2427
.SH ENVIRONMENT

‎jbmc/regression/jdiff/java-properties/test.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ old.jar --json-ui --show-properties --cover location
55
activate-multi-line-match
66
^EXIT=0$
77
^SIGNAL=0$
8-
"deletedFunctions": \[\n \{\n "name": "java::Test.obsolete:\(\)V",\n "properties": \[\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.obsolete:\(\)V": "18"\n \}\n \},\n "class": "coverage",\n "description": "block 1 \(lines Test.java:java::Test.obsolete:\(\)V:18\)",\n "expression": "false",\n "name": "java::Test.obsolete:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "modifiedFunctions": \[\n \{\n "name": "java::Test.<init>:\(\)V",\n "properties": \[\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.<init>:\(\)V": "6"\n \}\n \},\n "class": "coverage",\n "description": "block 2 \(lines Test.java:java::Test.<init>:\(\)V:6\)",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "6"\n }\n },\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.<init>:\(\)V": "4"\n \}\n \},\n "class": "coverage",\n "description": "block 3 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.2",\n "sourceLocation": \{\n "bytecodeIndex": "3",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "4"\n }\n },\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.<init>:\(\)V": "4"\n \}\n \},\n "class": "coverage",\n "description": "block 4 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.3",\n "sourceLocation": \{\n "bytecodeIndex": "5",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "4"\n }\n },\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.<init>:\(\)V": "4"\n \}\n \},\n "class": "coverage",\n "description": "block 5 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.4",\n "sourceLocation": \{\n "bytecodeIndex": "6",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "4"\n }\n },\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.<init>:\(\)V": "7"\n \}\n \},\n "class": "coverage",\n "description": "block 6 \(lines Test.java:java::Test.<init>:\(\)V:7\)",\n "expression": "false",\n "name": "java::Test.<init>:\(\)V.coverage.5",\n "sourceLocation": \{\n "bytecodeIndex": "7",\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "7"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.<init>:\(\)V",\n "line": "6"\n }\n },\n \{\n "name": "java::Test.<clinit>:\(\)V",\n "properties": \[\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.<clinit>:\(\)V": "3"\n \}\n \},\n "class": "coverage",\n "description": "block 1 \(lines Test.java:java::Test.<clinit>:\(\)V:3\)",\n "expression": "false",\n "name": "java::Test.<clinit>:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.<clinit>:\(\)V",\n "line": "3"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.<clinit>:\(\)V",\n "line": "3"\n }\n }\n ],\n "newFunctions": \[\n \{\n "name": "java::Test.newfun:\(\)V",\n "properties": \[\n \{\n "basicBlockLines": \{\n "Test.java": \{\n "java::Test.newfun:\(\)V": "18"\n \}\n \},\n "class": "coverage",\n "description": "block 1 \(lines Test.java:java::Test.newfun:\(\)V:18\)",\n "expression": "false",\n "name": "java::Test.newfun:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n
8+
\s*"deletedFunctions": \[\n\s*\{\n\s*"name": "java::Test.obsolete:\(\)V",\n\s*"properties": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.obsolete:\(\)V": "18"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 1 \(lines Test.java:java::Test.obsolete:\(\)V:18\)",\n\s*"expression": "false",\n\s*"name": "java::Test.obsolete:\(\)V.coverage.1",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.obsolete:\(\)V": \{\n\s*"id": "18"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "0",\n\s*"comment": "block 1 \(lines Test.java:java::Test.obsolete:\(\)V:18\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.obsolete:\(\)V",\n\s*"line": "18",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.obsolete:\(\)V.coverage.1"\n\s*\}\n\s*\}\n\s*\],\n\s*"sourceLocation": \{\n\s*"file": "Test.java",\n\s*"function": "java::Test.obsolete:\(\)V",\n\s*"line": "18"\n\s*\}\n\s*\}\n\s*\],\n\s*"modifiedFunctions": \[\n\s*\{\n\s*"name": "java::Test.<init>:\(\)V",\n\s*"properties": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.<init>:\(\)V": "6"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 2 \(lines Test.java:java::Test.<init>:\(\)V:6\)",\n\s*"expression": "false",\n\s*"name": "java::Test.<init>:\(\)V.coverage.1",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.<init>:\(\)V": \{\n\s*"id": "6"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "1",\n\s*"comment": "block 2 \(lines Test.java:java::Test.<init>:\(\)V:6\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.<init>:\(\)V",\n\s*"line": "6",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.<init>:\(\)V.coverage.1"\n\s*\}\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.<init>:\(\)V": "4"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 3 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n\s*"expression": "false",\n\s*"name": "java::Test.<init>:\(\)V.coverage.2",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.<init>:\(\)V": \{\n\s*"id": "4"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "3",\n\s*"comment": "block 3 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.<init>:\(\)V",\n\s*"line": "4",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.<init>:\(\)V.coverage.2"\n\s*\}\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.<init>:\(\)V": "4"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 4 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n\s*"expression": "false",\n\s*"name": "java::Test.<init>:\(\)V.coverage.3",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.<init>:\(\)V": \{\n\s*"id": "4"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "5",\n\s*"comment": "block 4 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.<init>:\(\)V",\n\s*"line": "4",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.<init>:\(\)V.coverage.3"\n\s*\}\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.<init>:\(\)V": "4"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 5 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n\s*"expression": "false",\n\s*"name": "java::Test.<init>:\(\)V.coverage.4",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.<init>:\(\)V": \{\n\s*"id": "4"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "6",\n\s*"comment": "block 5 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.<init>:\(\)V",\n\s*"line": "4",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.<init>:\(\)V.coverage.4"\n\s*\}\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.<init>:\(\)V": "7"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 6 \(lines Test.java:java::Test.<init>:\(\)V:7\)",\n\s*"expression": "false",\n\s*"name": "java::Test.<init>:\(\)V.coverage.5",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.<init>:\(\)V": \{\n\s*"id": "7"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "7",\n\s*"comment": "block 6 \(lines Test.java:java::Test.<init>:\(\)V:7\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.<init>:\(\)V",\n\s*"line": "7",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.<init>:\(\)V.coverage.5"\n\s*\}\n\s*\}\n\s*\],\n\s*"sourceLocation": \{\n\s*"file": "Test.java",\n\s*"function": "java::Test.<init>:\(\)V",\n\s*"line": "6"\n\s*\}\n\s*\},\n\s*\{\n\s*"name": "java::Test.<clinit>:\(\)V",\n\s*"properties": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.<clinit>:\(\)V": "3"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 1 \(lines Test.java:java::Test.<clinit>:\(\)V:3\)",\n\s*"expression": "false",\n\s*"name": "java::Test.<clinit>:\(\)V.coverage.1",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.<clinit>:\(\)V": \{\n\s*"id": "3"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "1",\n\s*"comment": "block 1 \(lines Test.java:java::Test.<clinit>:\(\)V:3\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.<clinit>:\(\)V",\n\s*"line": "3",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.<clinit>:\(\)V.coverage.1"\n\s*\}\n\s*\}\n\s*\],\n\s*"sourceLocation": \{\n\s*"file": "Test.java",\n\s*"function": "java::Test.<clinit>:\(\)V",\n\s*"line": "3"\n\s*\}\n\s*\}\n\s*\],\n\s*"newFunctions": \[\n\s*\{\n\s*"name": "java::Test.newfun:\(\)V",\n\s*"properties": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.newfun:\(\)V": "18"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 1 \(lines Test.java:java::Test.newfun:\(\)V:18\)",\n\s*"expression": "false",\n\s*"name": "java::Test.newfun:\(\)V.coverage.1",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.newfun:\(\)V": \{\n\s*"id": "18"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "0",\n\s*"comment": "block 1 \(lines Test.java:java::Test.newfun:\(\)V:18\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.newfun:\(\)V",\n\s*"line": "18",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.newfun:\(\)V.coverage.1"\n\s*\}\n\s*\}\n\s*\],\n\s*"sourceLocation": \{\n\s*"file": "Test.java",\n\s*"function": "java::Test.newfun:\(\)V",\n\s*"line": "18"\n\s*\}\n\s*\}\n\s*\],\n
99
--
1010
^warning: ignoring

‎regression/CMakeLists.txt‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,6 @@ add_subdirectory(goto-cc-multi-file)
8080
add_subdirectory(goto-cc-regression-gh-issue-5380)
8181
add_subdirectory(linking-goto-binaries)
8282
add_subdirectory(symtab2gb)
83-
add_subdirectory(symtab2gb-cbmc)
8483
add_subdirectory(solver-hardness)
8584
if(NOT WIN32)
8685
add_subdirectory(goto-ld)

‎regression/Makefile‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,6 @@ DIRS = cbmc-shadow-memory \
5353
goto-cc-regression-gh-issue-5380 \
5454
linking-goto-binaries \
5555
symtab2gb \
56-
symtab2gb-cbmc \
5756
solver-hardness \
5857
goto-ld \
5958
validate-trace-xml-schema \

‎regression/cbmc-cover/json-goals1/test.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
activate-multi-line-match
55
^EXIT=0$
66
^SIGNAL=0$
7-
\{\n\s*"goals": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\}\n\s*\],\n\s*"goalsCovered": 4,\n\s*"totalGoals": 4\n\s*\}
7+
\{\n\s*"goals": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){22}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){22}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){22}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){22}\},\n\s*"status": "satisfied"\n\s*\}\n\s*\],\n\s*"goalsCovered": 4,\n\s*"totalGoals": 4\n\s*\}
88
--
99
^warning: ignoring

‎regression/cbmc/json-interface1/test.desc‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ activate-multi-line-match
55
^EXIT=10$
66
^SIGNAL=0$
77
Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
8-
\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"sourceLocation": \{\n\s*"file": "main.c",\n\s*"function": "foo",\n\s*"line": "(8|11)",\n\s*"workingDirectory": ".*json-interface1"\n\s*\},\n\s*"status": "SUCCESS"\n\s*\}
9-
\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"sourceLocation": \{\n\s*"file": "main.c",\n\s*"function": "foo",\n\s*"line": "(8|11)",\n\s*"workingDirectory": ".*json-interface1"\n\s*\},\n\s*"status": "FAILURE",\n\s*"trace": \[
8+
\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"sourceLocation": \{\n\s*"comment": "assertion 0",\n\s*"file": "main.c",\n\s*"function": "foo",\n\s*"line": "(8|11)",\n\s*"pragma":.*\n\s*"propertyClass": "assertion",\n\s*"propertyId": "foo.assertion.\d+",\n\s*"workingDirectory": ".*json-interface1"\n\s*\},\n\s*"status": "SUCCESS"\n\s*\}
9+
\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"sourceLocation": \{\n\s*"comment": "assertion 0",\n\s*"file": "main.c",\n\s*"function": "foo",\n\s*"line": "(8|11)",\n\s*"pragma":.*\n\s*"propertyClass": "assertion",\n\s*"propertyId": "foo.assertion.\d+",\n\s*"workingDirectory": ".*json-interface1"\n\s*\},\n\s*"status": "FAILURE",\n\s*"trace": \[
1010
VERIFICATION FAILED
1111
--
1212
"property": "foo\.assertion\.2"

‎regression/cbmc/loophead-trace/test-json.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ test.c
44
activate-multi-line-match
55
^EXIT=10$
66
^SIGNAL=0$
7-
\s*\{\n\s* .*\n\s* "sourceLocation": \{\n\s* .*,\n\s* .*,\n\s* "line": "5",\n\s* .*\n\s* \},\n\s* "stepType": "loop-head",\n\s* .*\n\s*\},\n\s*\{\n\s* .*\n\s* "sourceLocation": \{\n\s* .*,\n\s* .*,\n\s* "line": "5",\n\s* .*\n\s* \},\n\s* "stepType": "loop-head",\n\s* .*\n\s*\},
7+
\s*\{\n\s* .*\n\s* "sourceLocation": \{\n\s* .*,\n\s* .*,\n\s* "line": "5",\n\s* .*,\n\s* .*\n\s* \},\n\s* "stepType": "loop-head",\n\s* .*\n\s*\},\n\s*\{\n\s* .*\n\s* "sourceLocation": \{\n\s* .*,\n\s* .*,\n\s* "line": "5",\n\s* .*,\n\s* .*\n\s* \},\n\s* "stepType": "loop-head",\n\s* .*\n\s*\},
88
--
99
--
1010
Ensure even with sliced formulas, we get a location only step for

‎regression/solver-hardness/guards/test.desc‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,9 @@ main.c
55
^SIGNAL=0$
66
^\[main.assertion.1\] line 12 should fail: FAILURE$
77
^VERIFICATION FAILED$
8-
\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"goto_symex::\\\\guard#1 ∧ goto_symex::\\\\guard#2","Source":\{"file":"main.c","function":"main","line":"\d+","workingDirectory":".*"\}\}
8+
\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"goto_symex::\\\\guard#1 ∧ goto_symex::\\\\guard#2","Source":\{"file":"main.c","function":"main","line":"\d+","pragma":.*,"propertyClass":.*,"propertyId":.*,"workingDirectory":".*"\}\}
99
--
1010
^warning: ignoring
11-
\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"true","Source":\{"file":"main.c","function":"main","line":"\d+","workingDirectory":".*"\}\}
11+
\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"true","Source":\{"file":"main.c","function":"main","line":"\d+","pragma":.*,"propertyClass":.*,"propertyId":.*,"workingDirectory":".*"\}\}
1212
--
1313
"true" must not yield any clauses.

‎regression/symtab2gb-cbmc/CMakeLists.txt‎

Lines changed: 0 additions & 3 deletions
This file was deleted.

0 commit comments

Comments
 (0)