CBMC
rewrite_union.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_REWRITE_UNION_H
13 #define CPROVER_GOTO_PROGRAMS_REWRITE_UNION_H
14 
15 #include <goto-programs/goto_functions.h>
16 
17 class exprt;
18 class goto_modelt;
19 
20 void rewrite_union(exprt &);
21 void rewrite_union(goto_functionst::goto_functiont &);
22 void rewrite_union(goto_functionst &);
23 void rewrite_union(goto_modelt &);
24 
25 #endif // CPROVER_GOTO_PROGRAMS_REWRITE_UNION_H
exprt
Base class for all expressions.
Definition: expr.h:55
goto_modelt
Definition: goto_model.h:25
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:27
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:24
rewrite_union
void rewrite_union(exprt &)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
Definition: rewrite_union.cpp:65
goto_functions.h