CBMC
rewrite_union.cpp File Reference

Symbolic Execution of ANSI-C. More...

+ Include dependency graph for rewrite_union.cpp:

Go to the source code of this file.

Functions

static bool have_to_rewrite_union (const exprt &expr)
 
void rewrite_union_address_of (exprt &expr)
 
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) More...
 
void rewrite_union (goto_functionst::goto_functiont &goto_function)
 
void rewrite_union (goto_functionst &goto_functions)
 
void rewrite_union (goto_modelt &goto_model)
 
static bool restore_union_rec (exprt &expr, const namespacet &ns)
 Undo the union access -> byte_extract replacement that rewrite_union did for the purpose of displaying expressions to users. More...
 
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. More...
 

Detailed Description

Symbolic Execution of ANSI-C.

Definition in file rewrite_union.cpp.

Function Documentation

◆ have_to_rewrite_union()

static bool have_to_rewrite_union ( const exprt expr)
static

Definition at line 23 of file rewrite_union.cpp.

◆ 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
exprexpression to inspect and possibly transform
nsnamespace

Definition at line 180 of file rewrite_union.cpp.

◆ restore_union_rec()

static bool restore_union_rec ( exprt expr,
const namespacet ns 
)
static

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

Parameters
exprexpression to inspect and possibly transform
nsnamespace
Returns
True if, and only if, the expression is unmodified

Definition at line 128 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.

◆ rewrite_union_address_of()

void rewrite_union_address_of ( exprt expr)

Definition at line 46 of file rewrite_union.cpp.