dfcc_pointer_equals.cpp File Reference

#include "dfcc_pointer_equals.h"
#include <util/c_types.h>
#include <util/cprover_prefix.h>
#include <util/expr_iterator.h>
#include <util/pointer_expr.h>
#include <util/prefix.h>
#include <util/replace_expr.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/suffix.h>
#include <util/symbol.h>
#include "dfcc_cfg_info.h"
#include "dfcc_library.h"

Include dependency graph for dfcc_pointer_equals.cpp:

Go to the source code of this file.

Classes
class	pointer_equality_visitort

Functions
void	rewrite_equal_exprt_to_pointer_equals (exprt &expr)
	Rewrites equal_exprt over pointers into calls to the front-end function __CPROVER_pointer_equals, at the expression level.

Function Documentation

rewrite_equal_exprt_to_pointer_equals()

void rewrite_equal_exprt_to_pointer_equals

(

exprt &

expr

)

Rewrites equal_exprt over pointers into calls to the front-end function __CPROVER_pointer_equals, at the expression level.

Meant to be Applied before GOTO conversion of function contract clauses, followed by rewrite_calls.

Definition at line 145 of file dfcc_pointer_equals.cpp.