cprover
|
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>
Go to the source code of this file.
Functions | |
static bool | have_to_rewrite_union (const exprt &expr, const namespacet &ns) |
void | rewrite_union_address_of (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... | |
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) |
Symbolic Execution of ANSI-C.
Definition in file rewrite_union.cpp.
|
static |
Definition at line 23 of file rewrite_union.cpp.
References namespace_baset::follow(), forall_operands, irept::id(), member_exprt::struct_op(), to_member_expr(), and exprt::type().
Referenced by rewrite_union(), and rewrite_union_address_of().
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)
Definition at line 71 of file rewrite_union.cpp.
References byte_extract_id(), byte_update_id(), namespace_baset::follow(), Forall_operands, from_integer(), have_to_rewrite_union(), irept::id(), index_type(), unary_exprt::op(), rewrite_union(), rewrite_union_address_of(), member_exprt::struct_op(), to_address_of_expr(), to_member_expr(), to_union_expr(), and exprt::type().
Referenced by jdiff_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), rewrite_union(), and rewrite_union_address_of().
void rewrite_union | ( | goto_functionst::goto_functiont & | goto_function, |
const namespacet & | ns | ||
) |
Definition at line 110 of file rewrite_union.cpp.
References Forall_goto_program_instructions, and rewrite_union().
void rewrite_union | ( | goto_functionst & | goto_functions, |
const namespacet & | ns | ||
) |
Definition at line 121 of file rewrite_union.cpp.
References Forall_goto_functions, and rewrite_union().
void rewrite_union | ( | goto_modelt & | goto_model | ) |
Definition at line 129 of file rewrite_union.cpp.
References goto_modelt::goto_functions, rewrite_union(), and goto_modelt::symbol_table.
void rewrite_union_address_of | ( | exprt & | expr, |
const namespacet & | ns | ||
) |
Definition at line 47 of file rewrite_union.cpp.
References have_to_rewrite_union(), irept::id(), dereference_exprt::pointer(), rewrite_union(), member_exprt::struct_op(), to_dereference_expr(), to_index_expr(), and to_member_expr().
Referenced by rewrite_union().