Skip to content

Commit 555bc9d

Browse files
peterschrammelpeterschrammel
committed
Factor out show_program into separate file
1 parent d4536ec commit 555bc9d

File tree

6 files changed

+128
-87
lines changed

6 files changed

+128
-87
lines changed

‎src/cbmc/bmc.cpp

Lines changed: 4 additions & 86 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
1818

1919
#include <langapi/language_util.h>
2020

21+
#include <goto-checker/show_program.h>
22+
2123
#include <goto-programs/graphml_witness.h>
2224
#include <goto-programs/json_goto_trace.h>
2325
#include <goto-programs/xml_goto_trace.h>
@@ -200,90 +202,6 @@ void bmct::report_failure()
200202
}
201203
}
202204

203-
void bmct::show_program()
204-
{
205-
unsigned count=1;
206-
207-
std::cout << "\n" << "Program constraints:" << "\n";
208-
209-
for(const auto &step : equation.SSA_steps)
210-
{
211-
std::cout << "// " << step.source.pc->location_number << " ";
212-
std::cout << step.source.pc->source_location.as_string() << "\n";
213-
const irep_idt &function = step.source.pc->function;
214-
215-
if(step.is_assignment())
216-
{
217-
std::string string_value = from_expr(ns, function, step.cond_expr);
218-
std::cout << "(" << count << ") " << string_value << "\n";
219-
220-
if(!step.guard.is_true())
221-
{
222-
std::string string_value = from_expr(ns, function, step.guard);
223-
std::cout << std::string(std::to_string(count).size()+3, ' ');
224-
std::cout << "guard: " << string_value << "\n";
225-
}
226-
227-
count++;
228-
}
229-
else if(step.is_assert())
230-
{
231-
std::string string_value = from_expr(ns, function, step.cond_expr);
232-
std::cout << "(" << count << ") ASSERT("
233-
<< string_value <<") " << "\n";
234-
235-
if(!step.guard.is_true())
236-
{
237-
std::string string_value = from_expr(ns, function, step.guard);
238-
std::cout << std::string(std::to_string(count).size()+3, ' ');
239-
std::cout << "guard: " << string_value << "\n";
240-
}
241-
242-
count++;
243-
}
244-
else if(step.is_assume())
245-
{
246-
std::string string_value = from_expr(ns, function, step.cond_expr);
247-
std::cout << "(" << count << ") ASSUME("
248-
<< string_value <<") " << "\n";
249-
250-
if(!step.guard.is_true())
251-
{
252-
std::string string_value = from_expr(ns, function, step.guard);
253-
std::cout << std::string(std::to_string(count).size()+3, ' ');
254-
std::cout << "guard: " << string_value << "\n";
255-
}
256-
257-
count++;
258-
}
259-
else if(step.is_constraint())
260-
{
261-
std::string string_value = from_expr(ns, function, step.cond_expr);
262-
std::cout << "(" << count << ") CONSTRAINT("
263-
<< string_value <<") " << "\n";
264-
265-
count++;
266-
}
267-
else if(step.is_shared_read() || step.is_shared_write())
268-
{
269-
std::string string_value = from_expr(ns, function, step.ssa_lhs);
270-
std::cout << "(" << count << ") SHARED_"
271-
<< (step.is_shared_write()?"WRITE":"READ")
272-
<< "(" << string_value <<")\n";
273-
274-
if(!step.guard.is_true())
275-
{
276-
std::string string_value = from_expr(ns, function, step.guard);
277-
std::cout << std::string(std::to_string(count).size()+3, ' ');
278-
std::cout << "guard: " << string_value << "\n";
279-
}
280-
281-
count++;
282-
}
283-
}
284-
}
285-
286-
287205
void bmct::get_memory_model()
288206
{
289207
const std::string mm=options.get_option("mm");
@@ -404,7 +322,7 @@ safety_checkert::resultt bmct::execute(
404322

405323
if(options.get_bool_option("program-only"))
406324
{
407-
show_program();
325+
show_program(ns, equation);
408326
return safety_checkert::resultt::SAFE;
409327
}
410328

@@ -507,7 +425,7 @@ void bmct::show()
507425

508426
if(options.get_bool_option("program-only"))
509427
{
510-
show_program();
428+
show_program(ns, equation);
511429
}
512430
}
513431

‎src/cbmc/bmc.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -212,7 +212,6 @@ class bmct:public safety_checkert
212212
const goto_functionst &goto_functions,
213213
prop_convt &solver);
214214
virtual resultt stop_on_fail(prop_convt &solver);
215-
virtual void show_program();
216215
virtual void report_success();
217216
virtual void report_failure();
218217

‎src/goto-checker/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
SRC = property_checker.cpp \
22
safety_checker.cpp \
3+
show_program.cpp \
34
# Empty last line
45

56
INCLUDES= -I ..

‎src/goto-checker/module_dependencies.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
goto-checker
22
goto-programs
33
goto-symex
4+
langapi # will go away
45
solvers
56
util

‎src/goto-checker/show_program.cpp

Lines changed: 102 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,102 @@
1+
/*******************************************************************\
2+
3+
Module: Output of the program (SSA) constraints
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Output of the program (SSA) constraints
11+
12+
#include "show_program.h"
13+
14+
#include <iostream>
15+
16+
#include <goto-symex/symex_target_equation.h>
17+
18+
#include <langapi/language_util.h>
19+
20+
21+
void show_program(const namespacet &ns, const symex_target_equationt &equation)
22+
{
23+
unsigned count=1;
24+
25+
std::cout << "\n" << "Program constraints:" << "\n";
26+
27+
for(const auto &step : equation.SSA_steps)
28+
{
29+
std::cout << "// " << step.source.pc->location_number << " ";
30+
std::cout << step.source.pc->source_location.as_string() << "\n";
31+
const irep_idt &function = step.source.pc->function;
32+
33+
if(step.is_assignment())
34+
{
35+
std::string string_value = from_expr(ns, function, step.cond_expr);
36+
std::cout << "(" << count << ") " << string_value << "\n";
37+
38+
if(!step.guard.is_true())
39+
{
40+
std::string string_value = from_expr(ns, function, step.guard);
41+
std::cout << std::string(std::to_string(count).size()+3, ' ');
42+
std::cout << "guard: " << string_value << "\n";
43+
}
44+
45+
count++;
46+
}
47+
else if(step.is_assert())
48+
{
49+
std::string string_value = from_expr(ns, function, step.cond_expr);
50+
std::cout << "(" << count << ") ASSERT("
51+
<< string_value <<") " << "\n";
52+
53+
if(!step.guard.is_true())
54+
{
55+
std::string string_value = from_expr(ns, function, step.guard);
56+
std::cout << std::string(std::to_string(count).size()+3, ' ');
57+
std::cout << "guard: " << string_value << "\n";
58+
}
59+
60+
count++;
61+
}
62+
else if(step.is_assume())
63+
{
64+
std::string string_value = from_expr(ns, function, step.cond_expr);
65+
std::cout << "(" << count << ") ASSUME("
66+
<< string_value <<") " << "\n";
67+
68+
if(!step.guard.is_true())
69+
{
70+
std::string string_value = from_expr(ns, function, step.guard);
71+
std::cout << std::string(std::to_string(count).size()+3, ' ');
72+
std::cout << "guard: " << string_value << "\n";
73+
}
74+
75+
count++;
76+
}
77+
else if(step.is_constraint())
78+
{
79+
std::string string_value = from_expr(ns, function, step.cond_expr);
80+
std::cout << "(" << count << ") CONSTRAINT("
81+
<< string_value <<") " << "\n";
82+
83+
count++;
84+
}
85+
else if(step.is_shared_read() || step.is_shared_write())
86+
{
87+
std::string string_value = from_expr(ns, function, step.ssa_lhs);
88+
std::cout << "(" << count << ") SHARED_"
89+
<< (step.is_shared_write()?"WRITE":"READ")
90+
<< "(" << string_value <<")\n";
91+
92+
if(!step.guard.is_true())
93+
{
94+
std::string string_value = from_expr(ns, function, step.guard);
95+
std::cout << std::string(std::to_string(count).size()+3, ' ');
96+
std::cout << "guard: " << string_value << "\n";
97+
}
98+
99+
count++;
100+
}
101+
}
102+
}

‎src/goto-checker/show_program.h

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
/*******************************************************************\
2+
3+
Module: Output of the program (SSA) constraints
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Output of the program (SSA) constraints
11+
12+
#ifndef CPROVER_GOTO_CHECKER_SHOW_PROGRAM_H
13+
#define CPROVER_GOTO_CHECKER_SHOW_PROGRAM_H
14+
15+
class namespacet;
16+
class symex_target_equationt;
17+
18+
void show_program(const namespacet &ns, const symex_target_equationt &equation);
19+
20+
#endif // CPROVER_GOTO_CHECKER_SHOW_PROGRAM_H

0 commit comments

Comments
 (0)