parameter_assignments.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Add parameter assignments
 
Author: Daniel Kroening
 
Date:   September 2015
 
\*******************************************************************/
 
 
#include "parameter_assignments.h"
 
#include <util/std_expr.h>
 
#include "goto_model.h"
 
class parameter_assignmentst
{
public:
  explicit parameter_assignmentst(symbol_table_baset &_symbol_table)
    : symbol_table(_symbol_table)
  {
  }
 
  void operator()(
    goto_functionst &goto_functions);
 
protected:
  symbol_table_baset &symbol_table;
 
  void do_function_calls(
    goto_programt &goto_program);
};
 
void parameter_assignmentst::do_function_calls(
  goto_programt &goto_program)
{
  Forall_goto_program_instructions(i_it, goto_program)
  {
    if(i_it->is_function_call())
    {
      // add x=y for f(y) where x is the parameter
      PRECONDITION(as_const(*i_it).call_function().id() == ID_symbol);
 
      const irep_idt &identifier =
        to_symbol_expr(as_const(*i_it).call_function()).get_identifier();
 
      // see if we have it
      const namespacet ns(symbol_table);
      const symbolt &function_symbol=ns.lookup(identifier);
      const code_typet &code_type=to_code_type(function_symbol.type);
 
      goto_programt tmp;
 
      for(std::size_t nr=0; nr<code_type.parameters().size(); nr++)
      {
        irep_idt p_identifier=code_type.parameters()[nr].get_identifier();
 
        if(p_identifier.empty())
          continue;
 
        if(nr < as_const(*i_it).call_arguments().size())
        {
          const symbolt &lhs_symbol=ns.lookup(p_identifier);
          symbol_exprt lhs=lhs_symbol.symbol_expr();
          exprt rhs = typecast_exprt::conditional_cast(
            as_const(*i_it).call_arguments()[nr], lhs.type());
          tmp.add(goto_programt::make_assignment(
            code_assignt(lhs, rhs), i_it->source_location()));
        }
      }
 
      std::size_t count=tmp.instructions.size();
      goto_program.insert_before_swap(i_it, tmp);
 
      for(; count!=0; count--) i_it++;
    }
  }
}
 
void parameter_assignmentst::operator()(goto_functionst &goto_functions)
{
  for(auto &gf_entry : goto_functions.function_map)
    do_function_calls(gf_entry.second.body);
}
 
void parameter_assignments(
  symbol_table_baset &symbol_table,
  goto_functionst &goto_functions)
{
  parameter_assignmentst rr(symbol_table);
  rr(goto_functions);
}
 
void parameter_assignments(goto_modelt &goto_model)
{
  parameter_assignmentst rr(goto_model.symbol_table);
  rr(goto_model.goto_functions);
}