cprover
rewrite_union.cpp File Reference

Symbolic Execution of ANSI-C. More...

#include "rewrite_union.h"
#include <util/arith_tools.h>
#include <util/std_expr.h>
#include <util/std_code.h>
#include <util/byte_operators.h>
#include <goto-programs/goto_model.h>
#include <util/c_types.h>
Include dependency graph for rewrite_union.cpp:

Go to the source code of this file.

Functions

static bool have_to_rewrite_union (const exprt &expr, const namespacet &ns)
 
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) More...
 
static void rewrite_union (goto_functionst::goto_functiont &goto_function, const namespacet &ns)
 
void rewrite_union (goto_functionst &goto_functions, const namespacet &ns)
 
void rewrite_union (goto_modelt &goto_model)
 

Detailed Description

Symbolic Execution of ANSI-C.

Definition in file rewrite_union.cpp.

Function Documentation

◆ have_to_rewrite_union()

static bool have_to_rewrite_union ( const exprt expr,
const namespacet ns 
)
static

◆ rewrite_union() [1/4]

◆ rewrite_union() [2/4]

static void rewrite_union ( goto_functionst::goto_functiont goto_function,
const namespacet ns 
)
static

Definition at line 80 of file rewrite_union.cpp.

References Forall_goto_program_instructions, and rewrite_union().

◆ rewrite_union() [3/4]

void rewrite_union ( goto_functionst goto_functions,
const namespacet ns 
)

Definition at line 91 of file rewrite_union.cpp.

References Forall_goto_functions, and rewrite_union().

◆ rewrite_union() [4/4]

void rewrite_union ( goto_modelt goto_model)