Skip to content

Commit de69684

Browse files
tautschnigtautschnig
authored
Merge pull request #2885 from peterschrammel/factor-out-program-only
Factor out program_only from bmct
2 parents dda0689 + a889a16 commit de69684

File tree

5 files changed

+127
-87
lines changed

5 files changed

+127
-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: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
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+
void show_program(const namespacet &ns, const symex_target_equationt &equation)
21+
{
22+
unsigned count = 1;
23+
24+
std::cout << "\n"
25+
<< "Program constraints:"
26+
<< "\n";
27+
28+
for(const auto &step : equation.SSA_steps)
29+
{
30+
std::cout << "// " << step.source.pc->location_number << " ";
31+
std::cout << step.source.pc->source_location.as_string() << "\n";
32+
const irep_idt &function = step.source.pc->function;
33+
34+
if(step.is_assignment())
35+
{
36+
std::string string_value = from_expr(ns, function, step.cond_expr);
37+
std::cout << "(" << count << ") " << string_value << "\n";
38+
39+
if(!step.guard.is_true())
40+
{
41+
std::string string_value = from_expr(ns, function, step.guard);
42+
std::cout << std::string(std::to_string(count).size() + 3, ' ');
43+
std::cout << "guard: " << string_value << "\n";
44+
}
45+
46+
count++;
47+
}
48+
else if(step.is_assert())
49+
{
50+
std::string string_value = from_expr(ns, function, step.cond_expr);
51+
std::cout << "(" << count << ") ASSERT(" << string_value << ") "
52+
<< "\n";
53+
54+
if(!step.guard.is_true())
55+
{
56+
std::string string_value = from_expr(ns, function, step.guard);
57+
std::cout << std::string(std::to_string(count).size() + 3, ' ');
58+
std::cout << "guard: " << string_value << "\n";
59+
}
60+
61+
count++;
62+
}
63+
else if(step.is_assume())
64+
{
65+
std::string string_value = from_expr(ns, function, step.cond_expr);
66+
std::cout << "(" << count << ") ASSUME(" << string_value << ") "
67+
<< "\n";
68+
69+
if(!step.guard.is_true())
70+
{
71+
std::string string_value = from_expr(ns, function, step.guard);
72+
std::cout << std::string(std::to_string(count).size() + 3, ' ');
73+
std::cout << "guard: " << string_value << "\n";
74+
}
75+
76+
count++;
77+
}
78+
else if(step.is_constraint())
79+
{
80+
std::string string_value = from_expr(ns, function, step.cond_expr);
81+
std::cout << "(" << count << ") CONSTRAINT(" << string_value << ") "
82+
<< "\n";
83+
84+
count++;
85+
}
86+
else if(step.is_shared_read() || step.is_shared_write())
87+
{
88+
std::string string_value = from_expr(ns, function, step.ssa_lhs);
89+
std::cout << "(" << count << ") SHARED_"
90+
<< (step.is_shared_write() ? "WRITE" : "READ") << "("
91+
<< string_value << ")\n";
92+
93+
if(!step.guard.is_true())
94+
{
95+
std::string string_value = from_expr(ns, function, step.guard);
96+
std::cout << std::string(std::to_string(count).size() + 3, ' ');
97+
std::cout << "guard: " << string_value << "\n";
98+
}
99+
100+
count++;
101+
}
102+
}
103+
}

‎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_SYMEX_SHOW_PROGRAM_H
13+
#define CPROVER_GOTO_SYMEX_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_SYMEX_SHOW_PROGRAM_H

0 commit comments

Comments
 (0)