#include "expr2statement_list.h"
#include <ansi-c/expr2c.h>
#include <util/namespace.h>
#include <util/std_expr.h>
#include <util/suffix.h>
#include <util/symbol.h>
#include <cstring>
#include <iostream>

Include dependency graph for expr2statement_list.cpp:

Macros
#define	AND 'A'
	STL code for an AND instruction. More...

#define	OR 'O'
	STL code for an OR instruction. More...

#define	XOR 'X'
	STL code for a XOR instruction. More...

#define	NOT_POSTFIX 'N'
	Postfix for any negated boolean instruction. More...

#define	NOT "NOT"
	STL code for a NOT instruction. More...

#define	OPERAND_SEPARATOR ' '
	Separator between the instruction code and it's operand. More...

#define	LINE_SEPARATOR ";\n"
	Separator between the end of an instruction and the next one. More...

#define	NESTING_OPEN_LINE_SEPARATOR "(;\n"
	Separator for the end of an instruction that introduces a new layer of nesting. More...

#define	NESTING_CLOSED_LINE_SEPARATOR ");\n"
	Separator for the end of an instruction that closes a nesting layer. More...

#define	REFERENCE_FLAG '#'
	Prefix for the reference to any variable. More...

#define	SCOPE_SEPARATOR "::"
	CBMC-internal separator for variable scopes. More...

Functions
static std::vector< exprt >	instrument_equal_operands (const exprt &lhs, const exprt &rhs)
	Modifies the parameters of a binary equal expression with the help of its symmetry properties. More...

static bool	is_not_bool (const exprt &expr)
	Checks if the expression or one of its parameters is not of type bool. More...

std::string	expr2stl (const exprt &expr, const namespacet &ns)
	Converts a given expression to human-readable STL code. More...

std::string	type2stl (const typet &type, const namespacet &ns)
	Converts a given type to human-readable STL code. More...

Macro Definition Documentation

◆ AND

#define AND 'A'

STL code for an AND instruction.

Definition at line 22 of file expr2statement_list.cpp.

◆ LINE_SEPARATOR

#define LINE_SEPARATOR ";\n"

Separator between the end of an instruction and the next one.

Definition at line 40 of file expr2statement_list.cpp.

◆ NESTING_CLOSED_LINE_SEPARATOR

#define NESTING_CLOSED_LINE_SEPARATOR ");\n"

Separator for the end of an instruction that closes a nesting layer.

Also known as the NESTING CLOSED instruction.

Definition at line 48 of file expr2statement_list.cpp.

◆ NESTING_OPEN_LINE_SEPARATOR

#define NESTING_OPEN_LINE_SEPARATOR "(;\n"

Separator for the end of an instruction that introduces a new layer of nesting.

Definition at line 44 of file expr2statement_list.cpp.

◆ NOT

#define NOT "NOT"

STL code for a NOT instruction.

Definition at line 34 of file expr2statement_list.cpp.

◆ NOT_POSTFIX

#define NOT_POSTFIX 'N'

Postfix for any negated boolean instruction.

Definition at line 31 of file expr2statement_list.cpp.

◆ OPERAND_SEPARATOR

#define OPERAND_SEPARATOR ' '

Separator between the instruction code and it's operand.

Definition at line 37 of file expr2statement_list.cpp.

◆ OR

#define OR 'O'

STL code for an OR instruction.

Definition at line 25 of file expr2statement_list.cpp.

◆ REFERENCE_FLAG

#define REFERENCE_FLAG '#'

Prefix for the reference to any variable.

Definition at line 51 of file expr2statement_list.cpp.

◆ SCOPE_SEPARATOR

#define SCOPE_SEPARATOR "::"

CBMC-internal separator for variable scopes.

Definition at line 54 of file expr2statement_list.cpp.

◆ XOR

#define XOR 'X'

STL code for a XOR instruction.

Definition at line 28 of file expr2statement_list.cpp.

Function Documentation

◆ expr2stl()

std::string expr2stl	(	const exprt &	expr,
		const namespacet &	ns
	)

Converts a given expression to human-readable STL code.

Parameters

expr	Expression to be converted.
ns	Namespace of the TIA application.

Returns: String with the STL representation of the given parameters.

Definition at line 108 of file expr2statement_list.cpp.

◆ instrument_equal_operands()

static std::vector<exprt> instrument_equal_operands	(	const exprt &	lhs,
		const exprt &	rhs
	)

static

Modifies the parameters of a binary equal expression with the help of its symmetry properties.

This function basically converts the operands to operands of a XOR expression so that the whole expression can be treated as such. This can reduce complexity in some cases.

Parameters

lhs	Left side of the binary expression.
rhs	Right side of the binary expression.

Returns: List of instrumented operands.

Definition at line 64 of file expr2statement_list.cpp.

◆ is_not_bool()

static bool is_not_bool ( const exprt & expr )

static

Checks if the expression or one of its parameters is not of type bool.

Parameters

expr	Expression to verify.

Returns: True if the expression and its operands are not or only partially of type bool, false otherwise.

Definition at line 98 of file expr2statement_list.cpp.

◆ type2stl()

std::string type2stl	(	const typet &	type,
		const namespacet &	ns
	)

Converts a given type to human-readable STL code.

Parameters

type	Type to be converted.
ns	Namespace of the TIA application.

Returns: String with the STL representation of the given type.

Definition at line 115 of file expr2statement_list.cpp.

Macros

Functions

Macro Definition Documentation

◆ AND

◆ LINE_SEPARATOR

◆ NESTING_CLOSED_LINE_SEPARATOR

◆ NESTING_OPEN_LINE_SEPARATOR

◆ NOT

◆ NOT_POSTFIX

◆ OPERAND_SEPARATOR

◆ OR

◆ REFERENCE_FLAG

◆ SCOPE_SEPARATOR

◆ XOR

Function Documentation

◆ expr2stl()

◆ instrument_equal_operands()

◆ is_not_bool()

◆ type2stl()