symex_dereference_state.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symbolic Execution of ANSI-C
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/

 
#include "symex_dereference_state.h"

const symbolt *
symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr)
{
  if(is_ssa_expr(expr))
  {
    const ssa_exprt &ssa_expr=to_ssa_expr(expr);
    if(ssa_expr.get_original_expr().id()!=ID_symbol)
      return nullptr;
 
    const symbolt &ptr_symbol=
      ns.lookup(to_ssa_expr(expr).get_object_name());
 
    const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
 
    const symbolt *symbol;
    if(!failed_symbol.empty() && !ns.lookup(failed_symbol, symbol))
    {
      symbolt sym=*symbol;
      symbolt *sym_ptr=nullptr;
      const ssa_exprt sym_expr =
        state.rename_ssa<L1>(ssa_exprt{sym.symbol_expr()}, ns).get();
      sym.name = sym_expr.get_identifier();
      state.symbol_table.move(sym, sym_ptr);
      return sym_ptr;
    }
  }
  else if(expr.id()==ID_symbol)
  {
    const symbolt &ptr_symbol=
      ns.lookup(to_symbol_expr(expr).get_identifier());
 
    const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
 
    const symbolt *symbol;
    if(!failed_symbol.empty() && !ns.lookup(failed_symbol, symbol))
    {
      symbolt sym=*symbol;
      symbolt *sym_ptr=nullptr;
      const ssa_exprt sym_expr =
        state.rename_ssa<L1>(ssa_exprt{sym.symbol_expr()}, ns).get();
      sym.name = sym_expr.get_identifier();
      state.symbol_table.move(sym, sym_ptr);
      return sym_ptr;
    }
  }
 
  return nullptr;
}

std::vector<exprt>
symex_dereference_statet::get_value_set(const exprt &expr) const
{
  return state.value_set.get_value_set(expr, ns);
}