39 if(it->is_backwards_goto())
41 unsigned loop_id=it->loop_number;
43 std::cout <<
"Loop " << function_identifier <<
"." << loop_id <<
":" 46 std::cout <<
" " << it->source_location <<
"\n";
56 if(it->is_backwards_goto())
58 unsigned loop_id=it->loop_number;
62 xmlt xml_loop(
"loop");
66 std::cout << xml_loop <<
"\n";
86 if(it->is_backwards_goto())
88 unsigned loop_id=it->loop_number;
94 loop[
"sourceLocation"]=
json(it->source_location);
118 std::cout <<
",\n" << json_result;
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
const std::string & id2string(const irep_idt &d)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
function_mapt function_map
xmlt xml(const source_locationt &location)
json_arrayt & make_array()
jsont & push_back(const jsont &json)
void show_loop_ids_json(ui_message_handlert::uit ui, const irep_idt &function_identifier, const goto_programt &goto_program, json_arrayt &loops)
void set_attribute(const std::string &attribute, unsigned value)
#define PRECONDITION(CONDITION)
A collection of goto functions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A generic container class for the GOTO intermediate representation of one function.
xmlt & new_element(const std::string &key)
#define UNREACHABLE
This should be used to mark dead code.
json_objectt & make_object()
#define forall_goto_program_instructions(it, program)
goto_functionst goto_functions
GOTO functions.
json_objectt json(const source_locationt &location)