CBMC: /home/runner/work/cbmc/cbmc/src/goto-programs/rewrite_union.cpp File Reference

CBMC

Loading...

Searching...

No Matches

rewrite_union.cpp File Reference

Symbolic Execution of ANSI-C. More...

#include "rewrite_union.h"
#include <util/arith_tools.h>
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <util/pointer_expr.h>
#include <util/pointer_offset_size.h>
#include <util/std_code.h>
#include <goto-programs/goto_model.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)

void rewrite_union_address_of (exprt &expr)

void rewrite_union (exprt &expr)

We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL, 0, v)

void rewrite_union (goto_functionst::goto_functiont &goto_function)

void rewrite_union (goto_functionst &goto_functions)

void rewrite_union (goto_modelt &goto_model)

static bool restore_union_rec (exprt &expr, const namespacet &ns)

Undo the union access -> byte_extract replacement that rewrite_union did for the purpose of displaying expressions to users.

void restore_union (exprt &expr, const namespacet &ns)

Undo the union access -> byte_extract replacement that rewrite_union did for the purpose of displaying expressions to users.

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 )

static

Definition at line 23 of file rewrite_union.cpp.

◆ restore_union()

void restore_union ( exprt & expr,

const namespacet & ns

)

Undo the union access -> byte_extract replacement that rewrite_union did for the purpose of displaying expressions to users.

Parameters: expr expression to inspect and possibly transform

ns namespace

Definition at line 180 of file rewrite_union.cpp.

◆ restore_union_rec()

static bool restore_union_rec ( exprt & expr,

const namespacet & ns

)

static

Undo the union access -> byte_extract replacement that rewrite_union did for the purpose of displaying expressions to users.

Parameters: expr expression to inspect and possibly transform

ns namespace

Returns: True if, and only if, the expression is unmodified

Definition at line 128 of file rewrite_union.cpp.

◆ rewrite_union() [1/4]

void rewrite_union ( exprt & expr )

We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL, 0, v)

Definition at line 68 of file rewrite_union.cpp.

◆ rewrite_union() [2/4]

void rewrite_union ( goto_functionst & goto_functions )

Definition at line 112 of file rewrite_union.cpp.

◆ rewrite_union() [3/4]

void rewrite_union ( goto_functionst::goto_functiont & goto_function )

Definition at line 101 of file rewrite_union.cpp.

◆ rewrite_union() [4/4]

void rewrite_union ( goto_modelt & goto_model )

Definition at line 118 of file rewrite_union.cpp.

◆ rewrite_union_address_of()

void rewrite_union_address_of ( exprt & expr )

Definition at line 46 of file rewrite_union.cpp.