21 const std::map<loop_idt, exprt> &invariant_map,
22 const std::map<
loop_idt, std::set<exprt>> &assigns_map,
23 const std::string &json_output_str,
36 INVARIANT(!invariant_map.empty(),
"No synthesized loop contracts to dump");
41 std::set<std::string> sources_set;
44 std::map<std::string, json_arrayt> function_map;
48 for(
const auto &invariant_entry : invariant_map)
51 invariant_entry.first.loop_number,
55 const auto source_file =
id2string(head->source_location().get_file());
57 if(sources_set.insert(source_file).second)
62 function_map.find(
id2string(head->source_location().get_function()));
63 if(it_function == function_map.end())
65 std::string function_name =
66 id2string(head->source_location().get_function());
71 function_map.emplace(function_name, loop_contracts_array).first;
73 json_arrayt &loop_contracts_array = it_function->second;
77 std::string inv_string =
78 "loop " + std::to_string(invariant_entry.first.loop_number + 1) +
87 const auto it_assigns = assigns_map.find(invariant_entry.first);
88 if(it_assigns != assigns_map.end())
90 std::string assign_string =
91 "loop " + std::to_string(invariant_entry.first.loop_number + 1) +
94 bool in_first_iter =
true;
95 for(
const auto &a : it_assigns->second)
103 in_first_iter =
false;
113 json_stream.
push_back(
"sources", json_sources);
118 for(
const auto &loop_contracts : function_map)
120 json_functions_object[loop_contracts.first] = loop_contracts.second;
122 json_functions.
push_back(json_functions_object);
123 json_stream.
push_back(
"functions", json_functions);
127 json_stream.
push_back(
"output", json_output);
void dump_loop_contracts(goto_modelt &goto_model, const std::map< loop_idt, exprt > &invariant_map, const std::map< loop_idt, std::set< exprt > > &assigns_map, const std::string &json_output_str, std::ostream &out)
goto_programt::targett get_loop_head(const unsigned int target_loop_number, goto_functiont &function)
Find and return the first instruction of the natural loop with loop_number in function.