#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:

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.

Classes

Functions

Function Documentation

◆ rewrite_equal_exprt_to_pointer_equals()