rewrite_union.h File Reference

#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) More...
void	rewrite_union (goto_functionst::goto_functiont &)
void	rewrite_union (goto_functionst &)
void	rewrite_union (goto_modelt &)

Detailed Description

Symbolic Execution

Definition in file rewrite_union.h.

Function Documentation

rewrite_union() [1/4]

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)

Definition at line 65 of file rewrite_union.cpp.

rewrite_union() [2/4]

void rewrite_union

(

goto_functionst &

)

Definition at line 109 of file rewrite_union.cpp.

rewrite_union() [3/4]

void rewrite_union

(

goto_functionst::goto_functiont &

)

Definition at line 98 of file rewrite_union.cpp.

rewrite_union() [4/4]

void rewrite_union

(

goto_modelt &

)

Definition at line 115 of file rewrite_union.cpp.