Skip to content

Commit 138f89c

Browse files
lucasccordeirolucasccordeiro
committed
use json file as suggested at github issue diffblue#187
Signed-off-by: Lucas Cordeiro <[email protected]>
1 parent 5bcc815 commit 138f89c

File tree

8 files changed

+21
-4330
lines changed

8 files changed

+21
-4330
lines changed

‎regression/cbmc-cover/location2/main.json

Lines changed: 1 addition & 196 deletions
Original file line numberDiff line numberDiff line change
@@ -1,197 +1,2 @@
1-
[
2-
{
3-
"program": "CBMC 5.5"
4-
},
5-
{
6-
"messageText": "CBMC version 5.5 64-bit x86_64 linux",
7-
"messageType": "STATUS-MESSAGE"
8-
},
9-
{
10-
"messageText": "Parsing main.c",
11-
"messageType": "STATUS-MESSAGE"
12-
},
13-
{
14-
"messageText": "<command-line>:0:0: warning: \"__STDC_VERSION__\" redefined",
15-
"messageType": "WARNING"
16-
},
17-
{
18-
"messageText": "<built-in>: note: this is the location of the previous definition",
19-
"messageType": "WARNING"
20-
},
21-
{
22-
"messageText": "Converting",
23-
"messageType": "STATUS-MESSAGE"
24-
},
25-
{
26-
"messageText": "Type-checking main",
27-
"messageType": "STATUS-MESSAGE"
28-
},
29-
{
30-
"messageText": "function `assert' is not declared",
31-
"messageType": "WARNING"
32-
},
33-
{
34-
"messageText": "Generating GOTO Program",
35-
"messageType": "STATUS-MESSAGE"
36-
},
37-
{
38-
"messageText": "Adding CPROVER library (x86_64)",
39-
"messageType": "STATUS-MESSAGE"
40-
},
41-
{
42-
"messageText": "Removal of function pointers and virtual functions",
43-
"messageType": "STATUS-MESSAGE"
44-
},
45-
{
46-
"messageText": "Partial Inlining",
47-
"messageType": "STATUS-MESSAGE"
48-
},
49-
{
50-
"messageText": "Generic Property Instrumentation",
51-
"messageType": "STATUS-MESSAGE"
52-
},
53-
{
54-
"messageText": "Instrumenting coverage goals",
55-
"messageType": "STATUS-MESSAGE"
56-
},
57-
{
58-
"messageText": "Starting Bounded Model Checking",
59-
"messageType": "STATUS-MESSAGE"
60-
},
61-
{
62-
"messageText": "size of program expression: 45 steps",
63-
"messageType": "STATUS-MESSAGE"
64-
},
65-
{
66-
"messageText": "Generated 4 VCC(s), 4 remaining after simplification",
67-
"messageType": "STATUS-MESSAGE"
68-
},
69-
{
70-
"messageText": "Passing problem to propositional reduction",
71-
"messageType": "STATUS-MESSAGE"
72-
},
73-
{
74-
"messageText": "converting SSA",
75-
"messageType": "STATUS-MESSAGE"
76-
},
77-
{
78-
"messageText": "Aiming to cover 4 goal(s)",
79-
"messageType": "STATUS-MESSAGE"
80-
},
81-
{
82-
"messageText": "Running propositional reduction",
83-
"messageType": "STATUS-MESSAGE"
84-
},
85-
{
86-
"messageText": "Post-processing",
87-
"messageType": "STATUS-MESSAGE"
88-
},
89-
{
90-
"messageText": "Solving with MiniSAT 2.2.1 with simplifier",
91-
"messageType": "STATUS-MESSAGE"
92-
},
93-
{
94-
"messageText": "265 variables, 522 clauses",
95-
"messageType": "STATUS-MESSAGE"
96-
},
97-
{
98-
"messageText": "SAT checker: instance is SATISFIABLE",
99-
"messageType": "STATUS-MESSAGE"
100-
},
101-
{
102-
"messageText": "Covered block 1",
103-
"messageType": "STATUS-MESSAGE"
104-
},
105-
{
106-
"messageText": "Covered block 3",
107-
"messageType": "STATUS-MESSAGE"
108-
},
109-
{
110-
"messageText": "Covered block 4",
111-
"messageType": "STATUS-MESSAGE"
112-
},
113-
{
114-
"messageText": "Solving with MiniSAT 2.2.1 with simplifier",
115-
"messageType": "STATUS-MESSAGE"
116-
},
117-
{
118-
"messageText": "265 variables, 0 clauses",
119-
"messageType": "STATUS-MESSAGE"
120-
},
121-
{
122-
"messageText": "SAT checker: instance is SATISFIABLE",
123-
"messageType": "STATUS-MESSAGE"
124-
},
125-
{
126-
"messageText": "Covered block 2",
127-
"messageType": "STATUS-MESSAGE"
128-
},
129-
{
130-
"messageText": "Runtime decision procedure: 0.001s",
131-
"messageType": "STATUS-MESSAGE"
132-
},
133-
{
134-
"goals": [
135-
{
136-
"description": "block 1",
137-
"goal": "main.coverage.1",
138-
"sourceLocation": {
139-
"file": "main.c",
140-
"function": "main",
141-
"line": "3"
142-
},
143-
"status": "satisfied"
144-
},
145-
{
146-
"description": "block 2",
147-
"goal": "main.coverage.2",
148-
"sourceLocation": {
149-
"file": "main.c",
150-
"function": "main",
151-
"line": "8"
152-
},
153-
"status": "satisfied"
154-
},
155-
{
156-
"description": "block 3",
157-
"goal": "main.coverage.3",
158-
"sourceLocation": {
159-
"file": "main.c",
160-
"function": "main",
161-
"line": "10"
162-
},
163-
"status": "satisfied"
164-
},
165-
{
166-
"description": "block 4",
167-
"goal": "main.coverage.4",
168-
"sourceLocation": {
169-
"file": "main.c",
170-
"function": "main",
171-
"line": "12"
172-
},
173-
"status": "satisfied"
174-
}
175-
],
176-
"goalsCovered": 4,
177-
"tests": [
178-
{
179-
"coveredGoals": [ "main.coverage.1", "main.coverage.3", "main.coverage.4" ],
180-
"inputs": [ ]
181-
},
182-
{
183-
"coveredGoals": [ "main.coverage.2" ],
184-
"inputs": [ ]
185-
}
186-
],
187-
"totalGoals": 4
188-
},
189-
{
190-
"messageText": "** 4 of 4 covered (100.0%)",
191-
"messageType": "STATUS-MESSAGE"
192-
},
193-
{
194-
"messageText": "** Used 2 iterations",
195-
"messageType": "STATUS-MESSAGE"
196-
}
1+
[ { "file": "main.c", "function": "main", "lines": [ {"number": 3}, {"number": 8}, {"number": 10}, {"number": 12} ] }
1972
]

‎regression/cbmc-cover/location3/main.json

Lines changed: 1 addition & 186 deletions
Original file line numberDiff line numberDiff line change
@@ -1,187 +1,2 @@
1-
[
2-
{
3-
"program": "CBMC 5.5"
4-
},
5-
{
6-
"messageText": "CBMC version 5.5 64-bit x86_64 linux",
7-
"messageType": "STATUS-MESSAGE"
8-
},
9-
{
10-
"messageText": "Parsing main.c",
11-
"messageType": "STATUS-MESSAGE"
12-
},
13-
{
14-
"messageText": "<command-line>:0:0: warning: \"__STDC_VERSION__\" redefined",
15-
"messageType": "WARNING"
16-
},
17-
{
18-
"messageText": "<built-in>: note: this is the location of the previous definition",
19-
"messageType": "WARNING"
20-
},
21-
{
22-
"messageText": "Converting",
23-
"messageType": "STATUS-MESSAGE"
24-
},
25-
{
26-
"messageText": "Type-checking main",
27-
"messageType": "STATUS-MESSAGE"
28-
},
29-
{
30-
"messageText": "function `assert' is not declared",
31-
"messageType": "WARNING"
32-
},
33-
{
34-
"messageText": "Generating GOTO Program",
35-
"messageType": "STATUS-MESSAGE"
36-
},
37-
{
38-
"messageText": "Adding CPROVER library (x86_64)",
39-
"messageType": "STATUS-MESSAGE"
40-
},
41-
{
42-
"messageText": "Removal of function pointers and virtual functions",
43-
"messageType": "STATUS-MESSAGE"
44-
},
45-
{
46-
"messageText": "Partial Inlining",
47-
"messageType": "STATUS-MESSAGE"
48-
},
49-
{
50-
"messageText": "Generic Property Instrumentation",
51-
"messageType": "STATUS-MESSAGE"
52-
},
53-
{
54-
"messageText": "Instrumenting coverage goals",
55-
"messageType": "STATUS-MESSAGE"
56-
},
57-
{
58-
"messageText": "Starting Bounded Model Checking",
59-
"messageType": "STATUS-MESSAGE"
60-
},
61-
{
62-
"messageText": "size of program expression: 45 steps",
63-
"messageType": "STATUS-MESSAGE"
64-
},
65-
{
66-
"messageText": "Generated 4 VCC(s), 4 remaining after simplification",
67-
"messageType": "STATUS-MESSAGE"
68-
},
69-
{
70-
"messageText": "Passing problem to propositional reduction",
71-
"messageType": "STATUS-MESSAGE"
72-
},
73-
{
74-
"messageText": "converting SSA",
75-
"messageType": "STATUS-MESSAGE"
76-
},
77-
{
78-
"messageText": "Aiming to cover 4 goal(s)",
79-
"messageType": "STATUS-MESSAGE"
80-
},
81-
{
82-
"messageText": "Running propositional reduction",
83-
"messageType": "STATUS-MESSAGE"
84-
},
85-
{
86-
"messageText": "Post-processing",
87-
"messageType": "STATUS-MESSAGE"
88-
},
89-
{
90-
"messageText": "Solving with MiniSAT 2.2.1 with simplifier",
91-
"messageType": "STATUS-MESSAGE"
92-
},
93-
{
94-
"messageText": "265 variables, 522 clauses",
95-
"messageType": "STATUS-MESSAGE"
96-
},
97-
{
98-
"messageText": "SAT checker: instance is SATISFIABLE",
99-
"messageType": "STATUS-MESSAGE"
100-
},
101-
{
102-
"messageText": "Covered block 1",
103-
"messageType": "STATUS-MESSAGE"
104-
},
105-
{
106-
"messageText": "Covered block 3",
107-
"messageType": "STATUS-MESSAGE"
108-
},
109-
{
110-
"messageText": "Covered block 4",
111-
"messageType": "STATUS-MESSAGE"
112-
},
113-
{
114-
"messageText": "Solving with MiniSAT 2.2.1 with simplifier",
115-
"messageType": "STATUS-MESSAGE"
116-
},
117-
{
118-
"messageText": "265 variables, 0 clauses",
119-
"messageType": "STATUS-MESSAGE"
120-
},
121-
{
122-
"messageText": "SAT checker: instance is SATISFIABLE",
123-
"messageType": "STATUS-MESSAGE"
124-
},
125-
{
126-
"messageText": "Covered block 2",
127-
"messageType": "STATUS-MESSAGE"
128-
},
129-
{
130-
"messageText": "Runtime decision procedure: 0.001s",
131-
"messageType": "STATUS-MESSAGE"
132-
},
133-
{
134-
"goals": [
135-
{
136-
"description": "block 1",
137-
"goal": "main.coverage.1",
138-
"sourceLocation": {
139-
"file": "main.c",
140-
"function": "main",
141-
"line": "3"
142-
},
143-
"status": "satisfied"
144-
},
145-
{
146-
"description": "block 2",
147-
"goal": "main.coverage.2",
148-
"sourceLocation": {
149-
"file": "main.c",
150-
"function": "main",
151-
"line": "8"
152-
},
153-
"status": "satisfied"
154-
},
155-
{
156-
"description": "block 4",
157-
"goal": "main.coverage.4",
158-
"sourceLocation": {
159-
"file": "main.c",
160-
"function": "main",
161-
"line": "12"
162-
},
163-
"status": "satisfied"
164-
}
165-
],
166-
"goalsCovered": 4,
167-
"tests": [
168-
{
169-
"coveredGoals": [ "main.coverage.1", "main.coverage.3", "main.coverage.4" ],
170-
"inputs": [ ]
171-
},
172-
{
173-
"coveredGoals": [ "main.coverage.2" ],
174-
"inputs": [ ]
175-
}
176-
],
177-
"totalGoals": 4
178-
},
179-
{
180-
"messageText": "** 4 of 4 covered (100.0%)",
181-
"messageType": "STATUS-MESSAGE"
182-
},
183-
{
184-
"messageText": "** Used 2 iterations",
185-
"messageType": "STATUS-MESSAGE"
186-
}
1+
[ { "file": "main.c", "function": "main", "lines": [ {"number": 3}, {"number": 8}, {"number": 12} ] }
1872
]

0 commit comments

Comments
 (0)