dfcc_pointer_equals.h File Reference

Instruments occurrences of pointer_equals predicates in programs encoding requires and ensures clauses of contracts. More...

#include <util/message.h>
#include <goto-programs/goto_program.h>

Include dependency graph for dfcc_pointer_equals.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	dfcc_pointer_equalst
	Rewrites calls to pointer_equals predicates into calls to the library implementation. More...

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.

Detailed Description

Instruments occurrences of pointer_equals predicates in programs encoding requires and ensures clauses of contracts.

Definition in file dfcc_pointer_equals.h.

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.