CBMC
rewrite_union.h File Reference

Symbolic Execution. More...

+ 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 &)
 
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. More...
 

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

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.