cprover
Loading...
Searching...
No Matches
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
16
17class exprt;
18class goto_modelt;
19
20void rewrite_union(exprt &);
24
25#endif // CPROVER_GOTO_PROGRAMS_REWRITE_UNION_H
Base class for all expressions.
Definition expr.h:54
A collection of goto functions.
::goto_functiont goto_functiont
Goto Programs with Functions.
void rewrite_union(exprt &)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...