CBMC
format_expr.cpp File Reference

Expression Pretty Printing. More...

#include "format_expr.h"
#include "arith_tools.h"
#include "bitvector_expr.h"
#include "byte_operators.h"
#include "expr_util.h"
#include "floatbv_expr.h"
#include "format_type.h"
#include "ieee_float.h"
#include "mathematical_expr.h"
#include "mp_arith.h"
#include "pointer_expr.h"
#include "string_utils.h"
#include <map>
#include <ostream>
+ Include dependency graph for format_expr.cpp:

Go to the source code of this file.

Classes

struct  infix_opt
 
class  format_expr_configt
 

Functions

static bool bracket_subexpression (const exprt &sub_expr, const exprt &expr)
 We use the precendences that most readers expect (i.e., the ones you learn in primary school), and stay clear of the surprising ones that C has. More...
 
static std::ostream & format_rec (std::ostream &os, const multi_ary_exprt &src)
 This formats a multi-ary expression, adding parentheses where indicated by bracket_subexpression. More...
 
static std::ostream & format_rec (std::ostream &os, const binary_exprt &src)
 This formats a binary expression, which we do as for multi-ary expressions. More...
 
static std::ostream & format_rec (std::ostream &os, const unary_exprt &src)
 This formats a unary expression, adding parentheses very aggressively. More...
 
static std::ostream & format_rec (std::ostream &os, const ternary_exprt &src)
 This formats a ternary expression. More...
 
static std::ostream & format_rec (std::ostream &os, const constant_exprt &src)
 This formats a constant. More...
 
std::ostream & fallback_format_rec (std::ostream &os, const exprt &expr)
 
void add_format_hook (irep_idt id, format_expr_configt::formattert formatter)
 
std::ostream & format_rec (std::ostream &os, const exprt &expr)
 Formats an expression in a generic syntax that is inspired by C/C++/Java, and is meant for debugging. More...
 

Variables

const std::map< irep_idt, infix_optinfix_map
 
format_expr_configt format_expr_config
 

Detailed Description

Expression Pretty Printing.

Definition in file format_expr.cpp.

Function Documentation

◆ add_format_hook()

void add_format_hook ( irep_idt  id,
format_expr_configt::formattert  formatter 
)

Definition at line 636 of file format_expr.cpp.

◆ bracket_subexpression()

static bool bracket_subexpression ( const exprt sub_expr,
const exprt expr 
)
static

We use the precendences that most readers expect (i.e., the ones you learn in primary school), and stay clear of the surprising ones that C has.

Definition at line 55 of file format_expr.cpp.

◆ fallback_format_rec()

std::ostream& fallback_format_rec ( std::ostream &  os,
const exprt expr 
)

Definition at line 234 of file format_expr.cpp.

◆ format_rec() [1/6]

static std::ostream& format_rec ( std::ostream &  os,
const binary_exprt src 
)
static

This formats a binary expression, which we do as for multi-ary expressions.

Definition at line 135 of file format_expr.cpp.

◆ format_rec() [2/6]

static std::ostream& format_rec ( std::ostream &  os,
const constant_exprt src 
)
static

This formats a constant.

Definition at line 172 of file format_expr.cpp.

◆ format_rec() [3/6]

std::ostream& format_rec ( std::ostream &  os,
const exprt expr 
)

Formats an expression in a generic syntax that is inspired by C/C++/Java, and is meant for debugging.

Definition at line 641 of file format_expr.cpp.

◆ format_rec() [4/6]

static std::ostream& format_rec ( std::ostream &  os,
const multi_ary_exprt src 
)
static

This formats a multi-ary expression, adding parentheses where indicated by bracket_subexpression.

Definition at line 95 of file format_expr.cpp.

◆ format_rec() [5/6]

static std::ostream& format_rec ( std::ostream &  os,
const ternary_exprt src 
)
static

This formats a ternary expression.

Definition at line 164 of file format_expr.cpp.

◆ format_rec() [6/6]

static std::ostream& format_rec ( std::ostream &  os,
const unary_exprt src 
)
static

This formats a unary expression, adding parentheses very aggressively.

Definition at line 142 of file format_expr.cpp.

Variable Documentation

◆ format_expr_config

format_expr_configt format_expr_config

Definition at line 634 of file format_expr.cpp.

◆ infix_map

const std::map<irep_idt, infix_opt> infix_map
Initial value:
= {
{ID_plus, {"+"}},
{ID_minus, {"-"}},
{ID_mult, {"*"}},
{ID_div, {"/"}},
{ID_equal, {"="}},
{ID_notequal, {u8"\u2260"}},
{ID_and, {u8"\u2227"}},
{ID_or, {u8"\u2228"}},
{ID_xor, {u8"\u2295"}},
{ID_implies, {u8"\u21d2"}},
{ID_le, {u8"\u2264"}},
{ID_ge, {u8"\u2265"}},
{ID_lt, {"<"}},
{ID_gt, {">"}},
}
uint64_t u8
Definition: bytecode_info.h:58

Definition at line 35 of file format_expr.cpp.