rewrite_union.h File Reference

Symbolic Execution. More...

#include <goto-programs/goto_functions.h>

Include dependency graph for rewrite_union.h:

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

Go to the source code of this file.

Functions
void	rewrite_union (exprt &)
	We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL, 0, v)
void	rewrite_union (goto_functionst::goto_functiont &)
void	rewrite_union (goto_functionst &)
void	rewrite_union (goto_modelt &)
void	restore_union (exprt &, const namespacet &)
	Undo the union access -> byte_extract replacement that rewrite_union did for the purpose of displaying expressions to users.

Detailed Description

Symbolic Execution.

Definition in file rewrite_union.h.

Function Documentation

restore_union()

void restore_union	(	exprt &	expr,
		const namespacet &	ns
	)

Undo the union access -> byte_extract replacement that rewrite_union did for the purpose of displaying expressions to users.

Parameters

expr	expression to inspect and possibly transform
ns	namespace

Definition at line 180 of file rewrite_union.cpp.

rewrite_union() [1/4]

void rewrite_union

(

exprt &

expr

)

We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL, 0, v)

Definition at line 68 of file rewrite_union.cpp.

rewrite_union() [2/4]

void rewrite_union

(

goto_functionst &

goto_functions

)

Definition at line 112 of file rewrite_union.cpp.

rewrite_union() [3/4]

void rewrite_union

(

goto_functionst::goto_functiont &

goto_function

)

Definition at line 101 of file rewrite_union.cpp.

rewrite_union() [4/4]

void rewrite_union

(

goto_modelt &

goto_model

)

Definition at line 118 of file rewrite_union.cpp.