17
17
18
18
#include < langapi/language_util.h>
19
19
20
-
21
20
void show_program (const namespacet &ns, const symex_target_equationt &equation)
22
21
{
23
- unsigned count= 1 ;
22
+ unsigned count = 1 ;
24
23
25
- std::cout << " \n " << " Program constraints:" << " \n " ;
24
+ std::cout << " \n "
25
+ << " Program constraints:"
26
+ << " \n " ;
26
27
27
28
for (const auto &step : equation.SSA_steps )
28
29
{
@@ -38,7 +39,7 @@ void show_program(const namespacet &ns, const symex_target_equationt &equation)
38
39
if (!step.guard .is_true ())
39
40
{
40
41
std::string string_value = from_expr (ns, function, step.guard );
41
- std::cout << std::string (std::to_string (count).size ()+ 3 , ' ' );
42
+ std::cout << std::string (std::to_string (count).size () + 3 , ' ' );
42
43
std::cout << " guard: " << string_value << " \n " ;
43
44
}
44
45
@@ -47,13 +48,13 @@ void show_program(const namespacet &ns, const symex_target_equationt &equation)
47
48
else if (step.is_assert ())
48
49
{
49
50
std::string string_value = from_expr (ns, function, step.cond_expr );
50
- std::cout << " (" << count << " ) ASSERT("
51
- << string_value << " ) " << " \n " ;
51
+ std::cout << " (" << count << " ) ASSERT(" << string_value << " ) "
52
+ << " \n " ;
52
53
53
54
if (!step.guard .is_true ())
54
55
{
55
56
std::string string_value = from_expr (ns, function, step.guard );
56
- std::cout << std::string (std::to_string (count).size ()+ 3 , ' ' );
57
+ std::cout << std::string (std::to_string (count).size () + 3 , ' ' );
57
58
std::cout << " guard: " << string_value << " \n " ;
58
59
}
59
60
@@ -62,13 +63,13 @@ void show_program(const namespacet &ns, const symex_target_equationt &equation)
62
63
else if (step.is_assume ())
63
64
{
64
65
std::string string_value = from_expr (ns, function, step.cond_expr );
65
- std::cout << " (" << count << " ) ASSUME("
66
- << string_value << " ) " << " \n " ;
66
+ std::cout << " (" << count << " ) ASSUME(" << string_value << " ) "
67
+ << " \n " ;
67
68
68
69
if (!step.guard .is_true ())
69
70
{
70
71
std::string string_value = from_expr (ns, function, step.guard );
71
- std::cout << std::string (std::to_string (count).size ()+ 3 , ' ' );
72
+ std::cout << std::string (std::to_string (count).size () + 3 , ' ' );
72
73
std::cout << " guard: " << string_value << " \n " ;
73
74
}
74
75
@@ -77,22 +78,22 @@ void show_program(const namespacet &ns, const symex_target_equationt &equation)
77
78
else if (step.is_constraint ())
78
79
{
79
80
std::string string_value = from_expr (ns, function, step.cond_expr );
80
- std::cout << " (" << count << " ) CONSTRAINT("
81
- << string_value << " ) " << " \n " ;
81
+ std::cout << " (" << count << " ) CONSTRAINT(" << string_value << " ) "
82
+ << " \n " ;
82
83
83
84
count++;
84
85
}
85
86
else if (step.is_shared_read () || step.is_shared_write ())
86
87
{
87
88
std::string string_value = from_expr (ns, function, step.ssa_lhs );
88
89
std::cout << " (" << count << " ) SHARED_"
89
- << (step.is_shared_write ()? " WRITE" : " READ" )
90
- << " ( " << string_value <<" )\n " ;
90
+ << (step.is_shared_write () ? " WRITE" : " READ" ) << " ( "
91
+ << string_value << " )\n " ;
91
92
92
93
if (!step.guard .is_true ())
93
94
{
94
95
std::string string_value = from_expr (ns, function, step.guard );
95
- std::cout << std::string (std::to_string (count).size ()+ 3 , ' ' );
96
+ std::cout << std::string (std::to_string (count).size () + 3 , ' ' );
96
97
std::cout << " guard: " << string_value << " \n " ;
97
98
}
98
99
0 commit comments