goto_function.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: A GOTO Function
 
Author: Daniel Kroening
 
Date: May 2018
 
\*******************************************************************/
 
 
#include "goto_function.h"
 
#include <util/namespace.h>
#include <util/symbol.h>
 
void get_local_identifiers(
  const goto_functiont &goto_function,
  std::set<irep_idt> &dest)
{
  goto_function.body.get_decl_identifiers(dest);
 
  // add parameters
  for(const auto &identifier : goto_function.parameter_identifiers)
  {
    if(!identifier.empty())
      dest.insert(identifier);
  }
}
void get_local_identifiers( {…}
 
void goto_functiont::validate(const namespacet &ns, const validation_modet vm)
  const
{
  for(const auto &identifier : parameter_identifiers)
  {
    DATA_CHECK_WITH_DIAGNOSTICS(
      vm,
      identifier.empty() || ns.lookup(identifier).is_parameter,
      "parameter should be marked 'is_parameter' in the symbol table",
      "affected parameter: ",
      identifier);
  }
 
  // function body must end with an END_FUNCTION instruction
  if(body_available())
  {
    DATA_CHECK(
      vm,
      body.instructions.back().is_end_function(),
      "last instruction should be of end function type");
  }
 
  body.validate(ns, vm);
}
void goto_functiont::validate(const namespacet &ns, const validation_modet vm) {…}