void show_goto_functions(
  const namespacet &ns,
  ui_message_handlert::uit ui,
  const goto_functionst &goto_functions)
{
  switch(ui)
  {
  case ui_message_handlert::XML_UI:
  {
    show_goto_functions_xmlt xml_show_functions(ns);
    xml_show_functions(goto_functions, std::cout);
  }
  break;

  case ui_message_handlert::JSON_UI:
  {
    show_goto_functions_jsont json_show_functions(ns);
    json_show_functions(goto_functions, std::cout);
  }
  break;

  case ui_message_handlert::PLAIN:
    goto_functions.output(ns, std::cout);
    break;
  }
}

void stack_depth(
  symbol_tablet &symbol_table,
  goto_functionst &goto_functions,
  const int depth)
{
  const symbol_exprt sym=add_stack_depth_symbol(symbol_table);
  const exprt depth_expr(from_integer(depth, sym.type()));

  Forall_goto_functions(f_it, goto_functions)
    if(f_it->second.body_available &&
        f_it->first!=CPROVER_PREFIX "initialize" &&
        f_it->first!=ID_main)
      stack_depth(f_it->second.body, sym, depth, depth_expr);

  // initialize depth to 0
  goto_functionst::function_mapt::iterator
    i_it=goto_functions.function_map.find(CPROVER_PREFIX "initialize");
  assert(i_it!=goto_functions.function_map.end());

  goto_programt &init=i_it->second.body;
  goto_programt::targett first=init.instructions.begin();
  goto_programt::targett it=init.insert_before(first);
  it->make_assignment();
  it->code=code_assignt(sym, from_integer(0, sym.type()));
  it->location=first->location;
  it->function=first->function;

  // update counters etc.
  goto_functions.update();
}

void add_cegis_library(symbol_tablet &st, goto_functionst &gf,
    message_handlert &msg, const size_t num_vars, const size_t num_consts,
    const size_t max_solution_size, const std::string &func_name)
{
  add_execute_placeholder(st, func_name, cegis_execute_type());
  std::set<irep_idt> functions;
  functions.insert(func_name);
  const std::string library_src(
      get_cegis_library_text(num_vars, num_consts, max_solution_size,
          func_name));

  add_library(library_src, st, msg);
  goto_convert(func_name, st, gf, msg);
  gf.compute_loop_numbers();
  gf.update();
  set_init_values(st, gf);
}

void nondet_static(
  const namespacet &ns,
  goto_functionst &goto_functions)
{
  nondet_static(ns, goto_functions, CPROVER_PREFIX "initialize");

  // update counters etc.
  goto_functions.update();
}

void remove_virtual_functionst::operator()(goto_functionst &functions)
{
  bool did_something=false;

  for(goto_functionst::function_mapt::iterator f_it=
      functions.function_map.begin();
      f_it!=functions.function_map.end();
      f_it++)
  {
    goto_programt &goto_program=f_it->second.body;

    if(remove_virtual_functions(goto_program))
      did_something=true;
  }

  if(did_something)
    functions.compute_location_numbers();
}

bool skip_loops(
  goto_functionst &goto_functions,
  const std::string &loop_ids,
  message_handlert &message_handler)
{
  messaget message(message_handler);

  loop_mapt loop_map;
  if(parse_loop_ids(loop_ids, loop_map))
  {
    message.error() << "Failed to parse loop ids" << messaget::eom;
    return true;
  }

  loop_mapt::const_iterator it=loop_map.begin();
  Forall_goto_functions(f_it, goto_functions)
  {
    if(it==loop_map.end() || it->first<f_it->first)
      break; // possible error handled below
    else if(it->first==f_it->first)
    {
      if(skip_loops(f_it->second.body, it->second, message))
        return true;
      ++it;
    }
  }
  if(it!=loop_map.end())
  {
    message.error() << "No function " << it->first << " in goto program"
                    << messaget::eom;
    return true;
  }

  // update counters etc.
  goto_functions.update();

  return false;
}

bool symex_parseoptionst::process_goto_program(
  const optionst &options,
  goto_functionst &goto_functions)
{
  try
  {
    namespacet ns(symbol_table);

    // do partial inlining
    status() << "Partial Inlining" << eom;
    goto_partial_inline(goto_functions, ns, ui_message_handler);

    // add generic checks
    status() << "Generic Property Instrumentation" << eom;
    goto_check(ns, options, goto_functions);

    // recalculate numbers, etc.
    goto_functions.update();

    // add loop ids
    goto_functions.compute_loop_numbers();

    // if we aim to cover, replace
    // all assertions by false to prevent simplification

    if(cmdline.isset("cover-assertions"))
      make_assertions_false(goto_functions);

    // show it?
    if(cmdline.isset("show-loops"))
    {
      show_loop_ids(get_ui(), goto_functions);
      return true;
    }

    // show it?
    if(cmdline.isset("show-goto-functions"))
    {
      goto_functions.output(ns, std::cout);
      return true;
    }
  }

  catch(const char *e)
  {
    error(e);
    return true;
  }

  catch(const std::string e)
  {
    error(e);
    return true;
  }

  catch(int)
  {
    return true;
  }

  catch(std::bad_alloc)
  {
    error() << "Out of memory" << eom;
    return true;
  }

  return false;
}

bool symex_parseoptionst::get_goto_program(
  const optionst &options,
  goto_functionst &goto_functions)
{
  if(cmdline.args.empty())
  {
    error() << "Please provide a program to verify" << eom;
    return true;
  }

  try
  {
    if(cmdline.args.size()==1 &&
       is_goto_binary(cmdline.args[0]))
    {
      status() << "Reading GOTO program from file" << eom;

      if(read_goto_binary(cmdline.args[0],
           symbol_table, goto_functions, get_message_handler()))
        return true;

      config.ansi_c.set_from_symbol_table(symbol_table);

      if(cmdline.isset("show-symbol-table"))
      {
        show_symbol_table();
        return true;
      }

      irep_idt entry_point=goto_functions.entry_point();

      if(symbol_table.symbols.find(entry_point)==symbol_table.symbols.end())
      {
        error() << "The goto binary has no entry point; please complete linking" << eom;
        return true;
      }
    }
    else if(cmdline.isset("show-parse-tree"))
    {
      if(cmdline.args.size()!=1)
      {
        error() << "Please give one source file only" << eom;
        return true;
      }

      std::string filename=cmdline.args[0];

      #ifdef _MSC_VER
      std::ifstream infile(widen(filename).c_str());
      #else
      std::ifstream infile(filename.c_str());
      #endif

      if(!infile)
      {
        error() << "failed to open input file `" << filename << "'" << eom;
        return true;
      }

      languaget *language=get_language_from_filename(filename);

      if(language==NULL)
      {
        error() << "failed to figure out type of file `" <<  filename << "'" << eom;
        return true;
      }

      status("Parsing", filename);

      if(language->parse(infile, filename, get_message_handler()))
      {
        error() << "PARSING ERROR" << eom;
        return true;
      }

      language->show_parse(std::cout);
      return true;
    }
    else
    {

      if(parse()) return true;
      if(typecheck()) return true;
      if(final()) return true;

      // we no longer need any parse trees or language files
      clear_parse();

      if(cmdline.isset("show-symbol-table"))
      {
        show_symbol_table();
        return true;
      }

      irep_idt entry_point=goto_functions.entry_point();

      if(symbol_table.symbols.find(entry_point)==symbol_table.symbols.end())
      {
        error() << "No entry point; please provide a main function" << eom;
        return true;
//.........这里部分代码省略.........

bool read_bin_goto_object_v3(
  std::istream &in,
  const std::string &filename,
  symbol_tablet &symbol_table,
  goto_functionst &functions,
  message_handlert &message_handler,
  irep_serializationt &irepconverter)
{
  std::size_t count = irepconverter.read_gb_word(in); // # of symbols

  for(std::size_t i=0; i<count; i++)
  {
    symbolt sym;

    irepconverter.reference_convert(in, sym.type);
    irepconverter.reference_convert(in, sym.value);
    irepconverter.reference_convert(in, sym.location);

    sym.name = irepconverter.read_string_ref(in);
    sym.module = irepconverter.read_string_ref(in);
    sym.base_name = irepconverter.read_string_ref(in);
    sym.mode = irepconverter.read_string_ref(in);
    sym.pretty_name = irepconverter.read_string_ref(in);

    // obsolete: symordering
    irepconverter.read_gb_word(in);

    std::size_t flags=irepconverter.read_gb_word(in);

    sym.is_weak = (flags &(1 << 16))!=0;
    sym.is_type = (flags &(1 << 15))!=0;
    sym.is_property = (flags &(1 << 14))!=0;
    sym.is_macro = (flags &(1 << 13))!=0;
    sym.is_exported = (flags &(1 << 12))!=0;
    sym.is_input = (flags &(1 << 11))!=0;
    sym.is_output = (flags &(1 << 10))!=0;
    sym.is_state_var = (flags &(1 << 9))!=0;
    sym.is_parameter = (flags &(1 << 8))!=0;
    sym.is_auxiliary = (flags &(1 << 7))!=0;
    // sym.binding = (flags &(1 << 6))!=0;
    sym.is_lvalue = (flags &(1 << 5))!=0;
    sym.is_static_lifetime = (flags &(1 << 4))!=0;
    sym.is_thread_local = (flags &(1 << 3))!=0;
    sym.is_file_local = (flags &(1 << 2))!=0;
    sym.is_extern = (flags &(1 << 1))!=0;
    sym.is_volatile = (flags &1)!=0;

    if(!sym.is_type && sym.type.id()==ID_code)
    {
      // makes sure there is an empty function
      // for every function symbol and fixes
      // the function types.
      functions.function_map[sym.name].type=to_code_type(sym.type);
    }

    symbol_table.add(sym);
  }

  count=irepconverter.read_gb_word(in); // # of functions

  for(std::size_t i=0; i<count; i++)
  {
    irep_idt fname=irepconverter.read_gb_string(in);
    goto_functionst::goto_functiont &f = functions.function_map[fname];

    typedef std::map<goto_programt::targett, std::list<unsigned> > target_mapt;
    target_mapt target_map;
    typedef std::map<unsigned, goto_programt::targett> rev_target_mapt;
    rev_target_mapt rev_target_map;

    bool hidden=false;

    std::size_t ins_count = irepconverter.read_gb_word(in); // # of instructions
    for(std::size_t i=0; i<ins_count; i++)
    {
      goto_programt::targett itarget = f.body.add_instruction();
      goto_programt::instructiont &instruction=*itarget;

      irepconverter.reference_convert(in, instruction.code);
      instruction.function = irepconverter.read_string_ref(in);
      irepconverter.reference_convert(in, instruction.source_location);
      instruction.type = (goto_program_instruction_typet)
                              irepconverter.read_gb_word(in);
      instruction.guard.make_nil();
      irepconverter.reference_convert(in, instruction.guard);
      irepconverter.read_string_ref(in); // former event
      instruction.target_number = irepconverter.read_gb_word(in);
      if(instruction.is_target() &&
         rev_target_map.insert(
           rev_target_map.end(),
           std::make_pair(instruction.target_number, itarget))->second!=itarget)
        assert(false);

      std::size_t t_count = irepconverter.read_gb_word(in); // # of targets
      for(std::size_t i=0; i<t_count; i++)
        // just save the target numbers
        target_map[itarget].push_back(irepconverter.read_gb_word(in));

      std::size_t l_count = irepconverter.read_gb_word(in); // # of labels

//.........这里部分代码省略.........

bool cbmc_parseoptionst::process_goto_program(
  const optionst &options,
  goto_functionst &goto_functions)
{
  try
  {
    namespacet ns(context);

    if(cmdline.isset("string-abstraction"))
      string_instrumentation(
        context, get_message_handler(), goto_functions);

    status("Function Pointer Removal");
    remove_function_pointers(ns, goto_functions,
      cmdline.isset("pointer-check"));

    status("Partial Inlining");
    // do partial inlining
    goto_partial_inline(goto_functions, ns, ui_message_handler);
    
    status("Generic Property Instrumentation");
    // add generic checks
    goto_check(ns, options, goto_functions);
    
    if(cmdline.isset("string-abstraction"))
    {
      status("String Abstraction");
      string_abstraction(context,
        get_message_handler(), goto_functions);
    }

    // add failed symbols
    // needs to be done before pointer analysis
    add_failed_symbols(context);
    
    if(cmdline.isset("pointer-check") ||
       cmdline.isset("show-value-sets"))
    {
      status("Pointer Analysis");
      value_set_analysist value_set_analysis(ns);
      value_set_analysis(goto_functions);

      // show it?
      if(cmdline.isset("show-value-sets"))
      {
        show_value_sets(get_ui(), goto_functions, value_set_analysis);
        return true;
      }

      status("Adding Pointer Checks");

      // add pointer checks
      pointer_checks(
        goto_functions, context, options, value_set_analysis);
    }

    // recalculate numbers, etc.
    goto_functions.update();

    // add loop ids
    goto_functions.compute_loop_numbers();
    
    // if we aim to cover, replace
    // all assertions by false to prevent simplification
    
    if(cmdline.isset("cover-assertions"))
      make_assertions_false(goto_functions);

    // show it?
    if(cmdline.isset("show-loops"))
    {
      show_loop_numbers(get_ui(), goto_functions);
      return true;
    }

    // show it?
    if(cmdline.isset("show-goto-functions"))
    {
      goto_functions.output(ns, std::cout);
      return true;
    }
  }

  catch(const char *e)
  {
    error(e);
    return true;
  }

  catch(const std::string e)
  {
    error(e);
    return true;
  }
  
  catch(int)
  {
    return true;
  }
  
//.........这里部分代码省略.........

bool cbmc_parse_optionst::process_goto_program(
  const optionst &options,
  goto_functionst &goto_functions)
{
  try
  {
    namespacet ns(symbol_table);
    
    // Remove inline assembler; this needs to happen before
    // adding the library.
    remove_asm(symbol_table, goto_functions);

    // add the library
    status() << "Adding CPROVER library (" 
             << config.ansi_c.arch << ")" << eom;
    link_to_library(symbol_table, goto_functions, ui_message_handler);

    if(cmdline.isset("string-abstraction"))
      string_instrumentation(
        symbol_table, get_message_handler(), goto_functions);

    // remove function pointers
    status() << "Function Pointer Removal" << eom;
    remove_function_pointers(symbol_table, goto_functions,
      cmdline.isset("pointer-check"));

    // full slice?
    if(cmdline.isset("full-slice"))
    {
      status() << "Performing a full slice" << eom;
      full_slicer(goto_functions, ns);
    }
  
    // do partial inlining
    status() << "Partial Inlining" << eom;
    goto_partial_inline(goto_functions, ns, ui_message_handler);
    
    // remove returns, gcc vectors, complex
    remove_returns(symbol_table, goto_functions);
    remove_vector(symbol_table, goto_functions);
    remove_complex(symbol_table, goto_functions);
    
    // add generic checks
    status() << "Generic Property Instrumentation" << eom;
    goto_check(ns, options, goto_functions);
    
    if(cmdline.isset("string-abstraction"))
    {
      status() << "String Abstraction" << eom;
      string_abstraction(symbol_table,
        get_message_handler(), goto_functions);
    }

    // add failed symbols
    // needs to be done before pointer analysis
    add_failed_symbols(symbol_table);
    
    // recalculate numbers, etc.
    goto_functions.update();

    // add loop ids
    goto_functions.compute_loop_numbers();
    
    // if we aim to cover assertions, replace
    // all assertions by false to prevent simplification
    
    if(cmdline.isset("cover") &&
       cmdline.get_value("cover")=="assertions")
      make_assertions_false(goto_functions);

    // show it?
    if(cmdline.isset("show-loops"))
    {
      show_loop_ids(get_ui(), goto_functions);
      return true;
    }

    // show it?
    if(cmdline.isset("show-goto-functions"))
    {
      goto_functions.output(ns, std::cout);
      return true;
    }
  }

  catch(const char *e)
  {
    error() << e << eom;
    return true;
  }

  catch(const std::string e)
  {
    error() << e << eom;
    return true;
  }
  
  catch(int)
  {
    return true;
//.........这里部分代码省略.........

void goto_fence_inserter_parse_optionst::instrument_goto_program(
  goto_functionst &goto_functions)
{
  optionst options;

  // unwind loops
  if(cmdline.isset("unwind"))
  {
    status() << "Unwinding loops" << eom;
    options.set_option("unwind", cmdline.get_value("unwind"));
  }

  // we add the library, as some analyses benefit

  status() << "Adding CPROVER library" << eom;
  link_to_library(symbol_table, goto_functions, ui_message_handler);

  namespacet ns(symbol_table);

  if( cmdline.isset("mm")
      || cmdline.isset("all-shared")
      || cmdline.isset("volatile")
      || cmdline.isset("pensieve")
      || cmdline.isset("naive")
      || cmdline.isset("all-shared-aeg") )
  {
    if(cmdline.isset("remove-function-pointers"))
    {
      status() << "remove soundly function pointers" << eom;
      remove_function_pointers(symbol_table, goto_functions,
        cmdline.isset("pointer-check"));
    }

    if(cmdline.isset("async"))
    {
      status() << "Replace pthread_creates by __CPROVER_ASYNC_0:" << eom;
      replace_async(ns, goto_functions);
      goto_functions.update();
    }

    // do partial inlining
    status() << "Partial Inlining" << eom;
    goto_partial_inline(goto_functions, ns, ui_message_handler);

    if(cmdline.isset("const-function-pointer-propagation"))
    {
      /* propagate const pointers to functions */
      status() << "Propagate Constant Function Pointers" << eom;
      propagate_const_function_pointers(symbol_table, goto_functions,
        get_message_handler());
    }

    // goto_functions.output(ns, std::cout);
    // return;
#if 0
    status() << "Function Pointer Removal" << eom;
    remove_function_pointers(symbol_table, goto_functions,
      cmdline.isset("pointer-check"));
#endif

#if 0
    // do partial inlining
    status() << "Partial Inlining" << eom;
    goto_partial_inline(goto_functions, ns, ui_message_handler);
#endif

    status() << "Pointer Analysis" << eom;
#ifdef POINTER_ANALYSIS_FI
    value_set_analysis_fit value_set_analysis(ns);
#else
    value_set_analysist value_set_analysis(ns);
#endif

#ifndef LOCAL_MAY
    value_set_analysis(goto_functions);
#endif

    status() << "Removing asm code" << eom;
    remove_asm(symbol_table, goto_functions);
    goto_functions.update();

    if(cmdline.isset("all-shared"))
    {
      status() << "Shared variables accesses detection" << eom;
      fence_all_shared(get_message_handler(), value_set_analysis, symbol_table,
        goto_functions);
      // simple analysis, coupled with script to insert;
      // does not transform the goto-binary
      return;
    }
    if(cmdline.isset("all-shared-aeg"))
    {
      status() << "Shared variables accesses detection (CF)" << eom;
      fence_all_shared_aeg(get_message_handler(), value_set_analysis,
        symbol_table, goto_functions);
      // simple analysis, coupled with script to insert;
      // does not transform the goto-binary
      return;
    }
    else if(cmdline.isset("volatile"))
//.........这里部分代码省略.........