show_goto_functions_xml.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Goto Program
 
Author: Thomas Kiley
 
\*******************************************************************/
 
 
#include "show_goto_functions_xml.h"
 
#include <iostream>
 
#include <util/cprover_prefix.h>
#include <util/prefix.h>
#include <util/xml_irep.h>
 
#include "goto_functions.h"
 
show_goto_functions_xmlt::show_goto_functions_xmlt(bool _list_only)
  : list_only(_list_only)
{}
 
xmlt show_goto_functions_xmlt::convert(
  const goto_functionst &goto_functions)
{
  xmlt xml_functions=xmlt("functions");
 
  const auto sorted = goto_functions.sorted();
 
  for(const auto &function_entry : sorted)
  {
    const irep_idt &function_name = function_entry->first;
    const goto_functionst::goto_functiont &function = function_entry->second;
 
    xmlt &xml_function=xml_functions.new_element("function");
    xml_function.set_attribute("name", id2string(function_name));
    xml_function.set_attribute_bool(
      "is_body_available", function.body_available());
    bool is_internal=
      has_prefix(id2string(function_name), CPROVER_PREFIX) ||
      has_prefix(id2string(function_name), "java::array[") ||
      has_prefix(id2string(function_name), "java::org.cprover") ||
      has_prefix(id2string(function_name), "java::java");
    xml_function.set_attribute_bool("is_internal", is_internal);
 
    if(list_only)
      continue;
 
    if(function.body_available())
    {
      xmlt &xml_instructions=xml_function.new_element("instructions");
      for(const goto_programt::instructiont &instruction :
        function.body.instructions)
      {
        xmlt &instruction_entry=xml_instructions.new_element("instruction");
 
        instruction_entry.set_attribute(
          "instruction_id", instruction.to_string());
 
        if(instruction.code().source_location().is_not_nil())
        {
          instruction_entry.new_element(
            xml(instruction.code().source_location()));
        }
 
        std::ostringstream instruction_builder;
        instruction.output(instruction_builder);
 
        xmlt &instruction_value=
          instruction_entry.new_element("instruction_value");
        instruction_value.data=instruction_builder.str();
        instruction_value.elements.clear();
      }
    }
  }
  return xml_functions;
}
 
void show_goto_functions_xmlt::operator()(
  const goto_functionst &goto_functions,
  std::ostream &out,
  bool append)
{
  if(append)
  {
    out << "\n";
  }
  out << convert(goto_functions);
}