cprover
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_SYMEX_REWRITE_UNION_H
13 #define CPROVER_GOTO_SYMEX_REWRITE_UNION_H
14 
16 
17 class exprt;
18 class namespacet;
19 class goto_functionst;
20 class goto_modelt;
21 
22 void rewrite_union(
23  exprt &expr,
24  const namespacet &ns);
25 
26 void rewrite_union(
27  goto_functionst::goto_functiont &goto_function,
28  const namespacet &ns);
29 
30 void rewrite_union(
32  const namespacet &ns);
33 void rewrite_union(goto_modelt &goto_model);
34 
35 #endif // CPROVER_GOTO_SYMEX_REWRITE_UNION_H
Goto Programs with Functions.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
void rewrite_union(exprt &expr, const namespacet &ns)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL, 0, v)
Base class for all expressions.
Definition: expr.h:42
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32