CBMC
goto_program2code.cpp File Reference

Dump Goto-Program as C/C++ Source. More...

#include "goto_program2code.h"
#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/c_types.h>
#include <util/expr_util.h>
#include <util/ieee_float.h>
#include <util/pointer_expr.h>
#include <util/prefix.h>
#include <util/simplify_expr.h>
#include <util/std_code.h>
#include <sstream>
+ Include dependency graph for goto_program2code.cpp:

Go to the source code of this file.

Functions

static bool has_labels (const codet &code)
 
static bool move_label_ifthenelse (exprt &expr, exprt &label_dest)
 

Detailed Description

Dump Goto-Program as C/C++ Source.

Definition in file goto_program2code.cpp.

Function Documentation

◆ has_labels()

static bool has_labels ( const codet code)
static

Definition at line 1643 of file goto_program2code.cpp.

◆ move_label_ifthenelse()

static bool move_label_ifthenelse ( exprt expr,
exprt label_dest 
)
static

Definition at line 1657 of file goto_program2code.cpp.