Skip to content

Commit e9d1f38

Browse files
peterschrammelpeterschrammel
committed
Clang-format
1 parent f23ac19 commit e9d1f38

File tree

4 files changed

+111
-102
lines changed

4 files changed

+111
-102
lines changed

‎src/cbmc/bmc.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -231,7 +231,8 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
231231
counterexample_beautificationt()(
232232
dynamic_cast<boolbvt &>(prop_conv), equation);
233233

234-
build_error_trace(error_trace, ns, equation, prop_conv, ui_message_handler);
234+
build_error_trace(
235+
error_trace, ns, equation, prop_conv, ui_message_handler);
235236
output_error_trace(error_trace, ns, trace_options(), ui_message_handler);
236237
output_graphml(resultt::UNSAFE, error_trace, equation, ns, options);
237238
}

‎src/cbmc/bmc_cover.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -211,7 +211,8 @@ bool bmc_covert::operator()()
211211

212212
// Do conversion to next solver layer
213213

214-
convert_symex_target_equation(bmc.equation, bmc.prop_conv, get_message_handler());
214+
convert_symex_target_equation(
215+
bmc.equation, bmc.prop_conv, get_message_handler());
215216
bmc.freeze_program_variables();
216217

217218
// get the conditions for these goals from formula

‎src/cbmc/fault_localization.cpp

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -249,7 +249,8 @@ fault_localizationt::run_decision_procedure(prop_convt &prop_conv)
249249

250250
auto solver_start=std::chrono::steady_clock::now();
251251

252-
convert_symex_target_equation(bmc.equation, bmc.prop_conv, get_message_handler());
252+
convert_symex_target_equation(
253+
bmc.equation, bmc.prop_conv, get_message_handler());
253254
bmc.freeze_program_variables();
254255

255256
freeze_guards();
@@ -285,8 +286,14 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()
285286
counterexample_beautificationt()(
286287
dynamic_cast<boolbvt &>(bmc.prop_conv), bmc.equation);
287288

288-
build_error_trace(bmc.error_trace, bmc.ns, bmc.equation, bmc.prop_conv, bmc.ui_message_handler);
289-
output_error_trace(bmc.error_trace, bmc.ns, bmc.trace_options(), bmc.ui_message_handler);
289+
build_error_trace(
290+
bmc.error_trace,
291+
bmc.ns,
292+
bmc.equation,
293+
bmc.prop_conv,
294+
bmc.ui_message_handler);
295+
output_error_trace(
296+
bmc.error_trace, bmc.ns, bmc.trace_options(), bmc.ui_message_handler);
290297
}
291298

292299
// localize faults

‎src/goto-checker/bmc_util.cpp

Lines changed: 97 additions & 97 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,8 @@ Author: Daniel Kroening, Peter Schrammel
1111

1212
#include "bmc_util.h"
1313

14-
#include <iostream>
1514
#include <fstream>
15+
#include <iostream>
1616

1717
#include <cbmc/symex_bmc.h>
1818

@@ -33,55 +33,57 @@ Author: Daniel Kroening, Peter Schrammel
3333
#include <util/make_unique.h>
3434
#include <util/ui_message.h>
3535

36-
37-
void build_error_trace(goto_tracet &goto_trace,
38-
const namespacet &ns,
39-
const symex_target_equationt &symex_target_equation,
40-
const prop_convt &prop_conv,
41-
ui_message_handlert &ui_message_handler)
36+
void build_error_trace(
37+
goto_tracet &goto_trace,
38+
const namespacet &ns,
39+
const symex_target_equationt &symex_target_equation,
40+
const prop_convt &prop_conv,
41+
ui_message_handlert &ui_message_handler)
4242
{
4343
messaget msg(ui_message_handler);
4444
msg.status() << "Building error trace" << messaget::eom;
4545

4646
build_goto_trace(symex_target_equation, prop_conv, ns, goto_trace);
4747
}
4848

49-
void output_error_trace(const goto_tracet &goto_trace, const namespacet &ns,
50-
const trace_optionst &trace_options,
51-
ui_message_handlert &ui_message_handler)
49+
void output_error_trace(
50+
const goto_tracet &goto_trace,
51+
const namespacet &ns,
52+
const trace_optionst &trace_options,
53+
ui_message_handlert &ui_message_handler)
5254
{
5355
messaget msg(ui_message_handler);
5456
switch(ui_message_handler.get_ui())
5557
{
56-
case ui_message_handlert::uit::PLAIN:
57-
msg.result() << "Counterexample:" << messaget::eom;
58-
show_goto_trace(msg.result(), ns, goto_trace, trace_options);
59-
msg.result() << messaget::eom;
60-
break;
58+
case ui_message_handlert::uit::PLAIN:
59+
msg.result() << "Counterexample:" << messaget::eom;
60+
show_goto_trace(msg.result(), ns, goto_trace, trace_options);
61+
msg.result() << messaget::eom;
62+
break;
6163

62-
case ui_message_handlert::uit::XML_UI:
63-
{
64-
xmlt xml;
65-
convert(ns, goto_trace, xml);
66-
msg.status() << xml;
67-
}
68-
break;
64+
case ui_message_handlert::uit::XML_UI:
65+
{
66+
xmlt xml;
67+
convert(ns, goto_trace, xml);
68+
msg.status() << xml;
69+
}
70+
break;
6971

70-
case ui_message_handlert::uit::JSON_UI:
71-
{
72-
json_stream_objectt &json_result =
73-
ui_message_handler.get_json_stream().push_back_stream_object();
74-
const goto_trace_stept &step=goto_trace.steps.back();
75-
json_result["property"] =
76-
json_stringt(step.pc->source_location.get_property_id());
77-
json_result["description"] =
78-
json_stringt(step.pc->source_location.get_comment());
79-
json_result["status"]=json_stringt("failed");
80-
json_stream_arrayt &json_trace =
81-
json_result.push_back_stream_array("trace");
82-
convert<json_stream_arrayt>(ns, goto_trace, json_trace, trace_options);
83-
}
84-
break;
72+
case ui_message_handlert::uit::JSON_UI:
73+
{
74+
json_stream_objectt &json_result =
75+
ui_message_handler.get_json_stream().push_back_stream_object();
76+
const goto_trace_stept &step = goto_trace.steps.back();
77+
json_result["property"] =
78+
json_stringt(step.pc->source_location.get_property_id());
79+
json_result["description"] =
80+
json_stringt(step.pc->source_location.get_comment());
81+
json_result["status"] = json_stringt("failed");
82+
json_stream_arrayt &json_trace =
83+
json_result.push_back_stream_array("trace");
84+
convert<json_stream_arrayt>(ns, goto_trace, json_trace, trace_options);
85+
}
86+
break;
8587
}
8688
}
8789

@@ -93,19 +95,19 @@ void output_graphml(
9395
const namespacet &ns,
9496
const optionst &options)
9597
{
96-
const std::string graphml=options.get_option("graphml-witness");
98+
const std::string graphml = options.get_option("graphml-witness");
9799
if(graphml.empty())
98100
return;
99101

100102
graphml_witnesst graphml_witness(ns);
101-
if(result==safety_checkert::resultt::UNSAFE)
103+
if(result == safety_checkert::resultt::UNSAFE)
102104
graphml_witness(goto_trace);
103-
else if(result==safety_checkert::resultt::SAFE)
105+
else if(result == safety_checkert::resultt::SAFE)
104106
graphml_witness(symex_target_equation);
105107
else
106108
return;
107109

108-
if(graphml=="-")
110+
if(graphml == "-")
109111
write_graphml(graphml_witness.graph(), std::cout);
110112
else
111113
{
@@ -126,33 +128,33 @@ void convert_symex_target_equation(
126128
equation.convert(prop_conv);
127129
}
128130

129-
std::unique_ptr<memory_model_baset> get_memory_model(
130-
const optionst &options,
131-
const namespacet &ns)
131+
std::unique_ptr<memory_model_baset>
132+
get_memory_model(const optionst &options, const namespacet &ns)
132133
{
133-
const std::string mm=options.get_option("mm");
134+
const std::string mm = options.get_option("mm");
134135

135-
if(mm.empty() || mm=="sc")
136+
if(mm.empty() || mm == "sc")
136137
return util_make_unique<memory_model_sct>(ns);
137-
else if(mm=="tso")
138+
else if(mm == "tso")
138139
return util_make_unique<memory_model_tsot>(ns);
139-
else if(mm=="pso")
140+
else if(mm == "pso")
140141
return util_make_unique<memory_model_psot>(ns);
141142
else
142143
{
143144
throw "invalid memory model '" + mm + "': use one of sc, tso, pso";
144145
}
145146
}
146147

147-
void setup_symex(symex_bmct &symex,
148-
const namespacet &ns,
149-
const optionst &options,
150-
ui_message_handlert &ui_message_handler)
148+
void setup_symex(
149+
symex_bmct &symex,
150+
const namespacet &ns,
151+
const optionst &options,
152+
ui_message_handlert &ui_message_handler)
151153
{
152154
messaget msg(ui_message_handler);
153155
const symbolt *init_symbol;
154156
if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol))
155-
symex.language_mode=init_symbol->mode;
157+
symex.language_mode = init_symbol->mode;
156158

157159
msg.status() << "Starting Bounded Model Checking" << messaget::eom;
158160

@@ -170,13 +172,12 @@ void slice(
170172
ui_message_handlert &ui_message_handler)
171173
{
172174
messaget msg(ui_message_handler);
173-
if(options.get_option("slice-by-trace")!="")
175+
if(options.get_option("slice-by-trace") != "")
174176
{
175177
symex_slice_by_tracet symex_slice_by_trace(ns);
176178

177-
symex_slice_by_trace.slice_by_trace
178-
(options.get_option("slice-by-trace"),
179-
symex_target_equation);
179+
symex_slice_by_trace.slice_by_trace(
180+
options.get_option("slice-by-trace"), symex_target_equation);
180181
}
181182
// any properties to check at all?
182183
if(symex_target_equation.has_threads())
@@ -190,24 +191,23 @@ void slice(
190191
{
191192
::slice(symex_target_equation);
192193
msg.statistics() << "slicing removed "
193-
<< symex_target_equation.count_ignored_SSA_steps()
194-
<< " assignments" << messaget::eom;
194+
<< symex_target_equation.count_ignored_SSA_steps()
195+
<< " assignments" << messaget::eom;
195196
}
196197
else
197198
{
198199
if(options.get_list_option("cover").empty())
199200
{
200201
simple_slice(symex_target_equation);
201202
msg.statistics() << "simple slicing removed "
202-
<< symex_target_equation.count_ignored_SSA_steps()
203-
<< " assignments" << messaget::eom;
203+
<< symex_target_equation.count_ignored_SSA_steps()
204+
<< " assignments" << messaget::eom;
204205
}
205206
}
206207
}
207-
msg.statistics() << "Generated "
208-
<< symex.get_total_vccs() <<" VCC(s), "
209-
<< symex.get_remaining_vccs()
210-
<< " remaining after simplification" << messaget::eom;
208+
msg.statistics() << "Generated " << symex.get_total_vccs() << " VCC(s), "
209+
<< symex.get_remaining_vccs()
210+
<< " remaining after simplification" << messaget::eom;
211211
}
212212

213213
void report_success(ui_message_handlert &ui_message_handler)
@@ -217,24 +217,24 @@ void report_success(ui_message_handlert &ui_message_handler)
217217

218218
switch(ui_message_handler.get_ui())
219219
{
220-
case ui_message_handlert::uit::PLAIN:
221-
break;
220+
case ui_message_handlert::uit::PLAIN:
221+
break;
222222

223-
case ui_message_handlert::uit::XML_UI:
224-
{
225-
xmlt xml("cprover-status");
226-
xml.data="SUCCESS";
227-
msg.result() << xml;
228-
}
229-
break;
223+
case ui_message_handlert::uit::XML_UI:
224+
{
225+
xmlt xml("cprover-status");
226+
xml.data = "SUCCESS";
227+
msg.result() << xml;
228+
}
229+
break;
230230

231-
case ui_message_handlert::uit::JSON_UI:
232-
{
233-
json_objectt json_result;
234-
json_result["cProverStatus"]=json_stringt("success");
235-
msg.result() << json_result;
236-
}
237-
break;
231+
case ui_message_handlert::uit::JSON_UI:
232+
{
233+
json_objectt json_result;
234+
json_result["cProverStatus"] = json_stringt("success");
235+
msg.result() << json_result;
236+
}
237+
break;
238238
}
239239
}
240240

@@ -245,23 +245,23 @@ void report_failure(ui_message_handlert &ui_message_handler)
245245

246246
switch(ui_message_handler.get_ui())
247247
{
248-
case ui_message_handlert::uit::PLAIN:
249-
break;
248+
case ui_message_handlert::uit::PLAIN:
249+
break;
250250

251-
case ui_message_handlert::uit::XML_UI:
252-
{
253-
xmlt xml("cprover-status");
254-
xml.data="FAILURE";
255-
msg.result() << xml;
256-
}
257-
break;
251+
case ui_message_handlert::uit::XML_UI:
252+
{
253+
xmlt xml("cprover-status");
254+
xml.data = "FAILURE";
255+
msg.result() << xml;
256+
}
257+
break;
258258

259-
case ui_message_handlert::uit::JSON_UI:
260-
{
261-
json_objectt json_result;
262-
json_result["cProverStatus"] = json_stringt("failure");
263-
msg.result() << json_result;
264-
}
265-
break;
259+
case ui_message_handlert::uit::JSON_UI:
260+
{
261+
json_objectt json_result;
262+
json_result["cProverStatus"] = json_stringt("failure");
263+
msg.result() << json_result;
264+
}
265+
break;
266266
}
267267
}

0 commit comments

Comments
 (0)