37 return pc->source_location.as_string() ==
38 other.
pc->source_location.as_string();
47 std::size_t ssa_index,
48 const exprt ssa_expression,
57 if(!pre_existing.second)
77 const exprt ssa_expression,
78 const std::vector<goto_programt::const_targett> &pcs)
94 for(
const auto &literal : bv)
114 std::size_t ssa_set_bit_offset = 0;
115 const std::size_t one = 1;
117 ++ssa_set_bit_offset;
125 if(ssa_step_hardness.empty())
129 for(
const auto &key_value_pair : ssa_step_hardness)
131 auto const &ssa = key_value_pair.first;
132 auto const &hardness = key_value_pair.second;
134 hardness_stats_json[
"SSA_expr"] =
json_stringt{ssa.ssa_expression};
135 hardness_stats_json[
"GOTO"] =
142 hardness_stats_json[
"GOTO_ID"] =
144 hardness_stats_json[
"Source"] =
json(ssa.pc->source_location);
147 sat_hardness_json[
"Clauses"] =
149 sat_hardness_json[
"Literals"] =
151 sat_hardness_json[
"Variables"] =
154 hardness_stats_json[
"SAT_hardness"] = sat_hardness_json;
156 json_stream_array.push_back(hardness_stats_json);
164 assertion_stats_json[
"SSA_expr"] =
171 assertion_stats_pc_json[
"GOTO"] =
173 assertion_stats_pc_json[
"Source"] =
json(pc->source_location);
174 assertion_stats_pcs_json.push_back(assertion_stats_pc_json);
176 assertion_stats_json[
"Sources"] = assertion_stats_pcs_json;
179 assertion_hardness_json[
"Clauses"] =
181 assertion_hardness_json[
"Literals"] =
186 assertion_stats_json[
"SAT_hardness"] = assertion_hardness_json;
188 json_stream_array.push_back(assertion_stats_json);
195 std::stringstream out;
196 auto instruction = *pc;
198 if(!instruction.labels.empty())
200 out <<
" // Labels:";
201 for(
const auto &label : instruction.labels)
205 if(instruction.is_target())
206 out << std::setw(6) << instruction.target_number <<
": ";
208 switch(instruction.type)
211 out <<
"NO INSTRUCTION TYPE SET";
216 if(!instruction.get_condition().is_true())
218 out <<
"IF " <<
format(instruction.get_condition()) <<
" THEN ";
223 if(instruction.is_incomplete_goto())
225 out <<
"(incomplete)";
229 for(
auto gt_it = instruction.targets.begin();
230 gt_it != instruction.targets.end();
233 if(gt_it != instruction.targets.begin())
235 out << (*gt_it)->target_number;
246 out <<
format(instruction.code);
251 if(instruction.is_assume())
256 out <<
format(instruction.get_condition());
264 out <<
"END_FUNCTION";
276 instruction.code.find(ID_exception_list).get_sub();
278 for(
const auto &ex : exception_list)
279 out <<
" " << ex.id();
282 if(instruction.code.operands().size() == 1)
283 out <<
": " <<
format(instruction.code.op0());
289 if(instruction.code.get_statement() == ID_exception_landingpad)
292 out <<
"EXCEPTION LANDING PAD (" <<
format(landingpad.catch_expr().type())
293 <<
' ' <<
format(landingpad.catch_expr()) <<
")";
295 else if(instruction.code.get_statement() == ID_push_catch)
297 out <<
"CATCH-PUSH ";
301 instruction.code.find(ID_exception_list).get_sub();
303 instruction.targets.size() == exception_list.size(),
304 "unexpected discrepancy between sizes of instruction"
305 "targets and exception list");
306 for(
auto gt_it = instruction.targets.begin();
307 gt_it != instruction.targets.end();
310 if(gt_it != instruction.targets.begin())
312 out << exception_list[i].id() <<
"->" << (*gt_it)->target_number;
315 else if(instruction.code.get_statement() == ID_pop_catch)
327 out <<
"ATOMIC_BEGIN";
335 out <<
"START THREAD " << instruction.get_target()->target_number;
348 std::stringstream ss;