CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
rewrite_union.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: 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
17class exprt;
18class goto_modelt;
19
20void rewrite_union(exprt &);
21void rewrite_union(goto_functionst::goto_functiont &);
22void rewrite_union(goto_functionst &);
23void rewrite_union(goto_modelt &);
24
25void restore_union(exprt &, const namespacet &);
26
27#endif // CPROVER_GOTO_PROGRAMS_REWRITE_UNION_H
exprt
Base class for all expressions.
Definition expr.h:56
goto_functionst
A collection of goto functions.
Definition goto_functions.h:25
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition goto_functions.h:27
goto_modelt
Definition goto_model.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
goto_functions.h
Goto Programs with Functions.
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:68
restore_union
void restore_union(exprt &, const namespacet &)
Undo the union access -> byte_extract replacement that rewrite_union did for the purpose of displayin...
Definition rewrite_union.cpp:180