rewrite_index.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Pointer Dereferencing
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#include "rewrite_index.h"
 
#include <util/pointer_expr.h>
#include <util/std_expr.h>
 
dereference_exprt rewrite_index(const index_exprt &index_expr)
{
  dereference_exprt result(
    plus_exprt(index_expr.array(), index_expr.index()), index_expr.type());
  result.add_source_location()=index_expr.source_location();
  return result;
}