add_failed_symbols.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Pointer Dereferencing
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#include "add_failed_symbols.h"
 
#include <util/c_types.h>
#include <util/namespace.h>
#include <util/std_expr.h>
#include <util/symbol.h>
#include <util/symbol_table_base.h>
 
#include <list>
 
irep_idt failed_symbol_id(const irep_idt &id)
{
  return id2string(id)+"$object";
}
 
void add_failed_symbol(symbolt &symbol, symbol_table_baset &symbol_table)
{
  if(symbol.type.id()==ID_pointer)
  {
    symbolt new_symbol;
    new_symbol.is_lvalue=true;
    new_symbol.module=symbol.module;
    new_symbol.mode=symbol.mode;
    new_symbol.base_name=failed_symbol_id(symbol.base_name);
    new_symbol.name=failed_symbol_id(symbol.name);
    new_symbol.type = to_pointer_type(symbol.type).base_type();
    new_symbol.value.make_nil();
    new_symbol.type.set(ID_C_is_failed_symbol, true);
 
    symbol.type.set(ID_C_failed_symbol, new_symbol.name);
 
    if(new_symbol.type.id()==ID_pointer)
      add_failed_symbol(new_symbol, symbol_table); // recursive call
 
    symbol_table.insert(std::move(new_symbol));
  }
}
 
void add_failed_symbol_if_needed(
  const symbolt &symbol, symbol_table_baset &symbol_table)
{
  if(!symbol.is_lvalue)
    return;
 
  if(!symbol.type.get(ID_C_failed_symbol).empty())
    return;
 
  add_failed_symbol(symbol_table.get_writeable_ref(symbol.name), symbol_table);
}
 
void add_failed_symbols(symbol_table_baset &symbol_table)
{
  // the symbol table iterators are not stable, and
  // we are adding new symbols, this
  // is why we need a list of pointers
  std::list<const symbolt *> symbol_list;
  for(auto &named_symbol : symbol_table.symbols)
    symbol_list.push_back(&(named_symbol.second));
 
  for(const symbolt *symbol : symbol_list)
    add_failed_symbol_if_needed(*symbol, symbol_table);
}
 
optionalt<symbol_exprt>
get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
{
  const symbolt &symbol=ns.lookup(expr);
  irep_idt failed_symbol_id=symbol.type.get(ID_C_failed_symbol);
 
  if(failed_symbol_id.empty())
    return {};
 
  const symbolt &failed_symbol=ns.lookup(failed_symbol_id);
 
  return symbol_exprt(failed_symbol_id, failed_symbol.type);
}