Skip to content

Commit 28ca28d

Browse files
Test for java-specific output in JSON
In particular, booleans are now printed as true/false instead of 0/1; NULL as null, and pointer types as their respective structs.
1 parent 49526f7 commit 28ca28d

File tree

3 files changed

+17
-0
lines changed

3 files changed

+17
-0
lines changed
292 Bytes
Binary file not shown.
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
public class Test {
2+
boolean test(Object x) {
3+
if(x==null)
4+
return false;
5+
return true;
6+
}
7+
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
Test.class
3+
--cover location --trace --json-ui --function Test.test
4+
activate-multi-line-match
5+
EXIT=0
6+
SIGNAL=0
7+
"outputID": "return",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "output",\n *"thread": 0,\n *"values": \[\n *\{\n *"binary": "00000000",\n *"data": "false",\n *"name": "integer",\n *"type": "boolean",\n *"width": 8
8+
"inputID": "arg1a",\n *"internal": true,\n *"mode": "java",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "input",\n *"thread": 0,\n *"values": \[\n *\{\n *"data": "null",\n *"name": "pointer",\n *"type": "struct java\.lang\.Object \{ __CPROVER_string @class_identifier; boolean @lock; \} \*"
9+
--
10+
^warning: ignoring

0 commit comments

Comments
 (0)