Skip to content

Commit 7b139dd

Browse files
peterschrammelpeterschrammel
committed
Factor out show_program into separate file
1 parent 946abb8 commit 7b139dd

File tree

5 files changed

+126
-87
lines changed

5 files changed

+126
-87
lines changed

‎src/cbmc/bmc.cpp

Lines changed: 3 additions & 86 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
2424

2525
#include <goto-symex/build_goto_trace.h>
2626
#include <goto-symex/memory_model_pso.h>
27+
#include <goto-symex/show_program.h>
2728
#include <goto-symex/slice.h>
2829
#include <goto-symex/slice_by_trace.h>
2930

@@ -200,90 +201,6 @@ void bmct::report_failure()
200201
}
201202
}
202203

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-
287204
void bmct::get_memory_model()
288205
{
289206
const std::string mm=options.get_option("mm");
@@ -404,7 +321,7 @@ safety_checkert::resultt bmct::execute(
404321

405322
if(options.get_bool_option("program-only"))
406323
{
407-
show_program();
324+
show_program(ns, equation);
408325
return safety_checkert::resultt::SAFE;
409326
}
410327

@@ -507,7 +424,7 @@ void bmct::show()
507424

508425
if(options.get_bool_option("program-only"))
509426
{
510-
show_program();
427+
show_program(ns, equation);
511428
}
512429
}
513430

‎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-symex/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ SRC = auto_objects.cpp \
1111
postcondition.cpp \
1212
precondition.cpp \
1313
rewrite_union.cpp \
14+
show_program.cpp \
1415
slice.cpp \
1516
slice_by_trace.cpp \
1617
symex_assign.cpp \

‎src/goto-symex/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-symex/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)