simplify_expr.cpp File Reference

#include "simplify_expr.h"
#include <algorithm>
#include "bitvector_expr.h"
#include "byte_operators.h"
#include "c_types.h"
#include "config.h"
#include "expr_util.h"
#include "fixedbv.h"
#include "floatbv_expr.h"
#include "invariant.h"
#include "mathematical_expr.h"
#include "namespace.h"
#include "pointer_expr.h"
#include "pointer_offset_size.h"
#include "pointer_offset_sum.h"
#include "rational.h"
#include "rational_tools.h"
#include "simplify_utils.h"
#include "std_expr.h"
#include "string_expr.h"
#include "simplify_expr_class.h"

Include dependency graph for simplify_expr.cpp:

Go to the source code of this file.

Functions
static simplify_exprt::resultt	simplify_string_endswith (const function_application_exprt &expr, const namespacet &ns)
	Simplify String.endsWith function when arguments are constant.
static simplify_exprt::resultt	simplify_string_contains (const function_application_exprt &expr, const namespacet &ns)
	Simplify String.contains function when arguments are constant.
static simplify_exprt::resultt	simplify_string_is_empty (const function_application_exprt &expr, const namespacet &ns)
	Simplify String.isEmpty function when arguments are constant.
static simplify_exprt::resultt	simplify_string_compare_to (const function_application_exprt &expr, const namespacet &ns)
	Simplify String.compareTo function when arguments are constant.
static simplify_exprt::resultt	simplify_string_index_of (const function_application_exprt &expr, const namespacet &ns, const bool search_from_end)
	Simplify String.indexOf function when arguments are constant.
static simplify_exprt::resultt	simplify_string_char_at (const function_application_exprt &expr, const namespacet &ns)
	Simplify String.charAt function when arguments are constant.
static bool	lower_case_string_expression (array_exprt &string_data)
	Take the passed-in constant string array and lower-case every character.
static simplify_exprt::resultt	simplify_string_equals_ignore_case (const function_application_exprt &expr, const namespacet &ns)
	Simplify String.equalsIgnorecase function when arguments are constant.
static simplify_exprt::resultt	simplify_string_startswith (const function_application_exprt &expr, const namespacet &ns)
	Simplify String.startsWith function when arguments are constant.
bool	simplify (exprt &expr, const namespacet &ns)
exprt	simplify_expr (exprt src, const namespacet &ns)

Function Documentation

lower_case_string_expression()

static bool lower_case_string_expression ( array_exprt &  string_data )

static

Take the passed-in constant string array and lower-case every character.

Definition at line 561 of file simplify_expr.cpp.

simplify()

bool simplify	(	exprt &	expr,
		const namespacet &	ns
	)

Returns

returns true if expression unchanged; returns false if changed

Definition at line 3246 of file simplify_expr.cpp.

simplify_expr()

exprt simplify_expr	(	exprt	src,
		const namespacet &	ns
	)

Definition at line 3251 of file simplify_expr.cpp.

simplify_string_char_at()

static simplify_exprt::resultt simplify_string_char_at ( const function_application_exprt &  expr, const namespacet &  ns  )

static

Simplify String.charAt function when arguments are constant.

Parameters

expr	the expression to simplify
ns	namespace

Returns

: the modified expression or an unchanged expression

Definition at line 521 of file simplify_expr.cpp.

simplify_string_compare_to()

static simplify_exprt::resultt simplify_string_compare_to ( const function_application_exprt &  expr, const namespacet &  ns  )

static

Simplify String.compareTo function when arguments are constant.

The behaviour is similar to the implementation in OpenJDK: http://hg.openjdk.java.net/jdk8/jdk8/jdk/file/687fd7c7986d/src/share/classes/java/lang/String.java#l1140

Parameters

expr	the expression to simplify
ns	namespace

Returns

the modified expression or an unchanged expression

Definition at line 327 of file simplify_expr.cpp.

simplify_string_contains()

static simplify_exprt::resultt simplify_string_contains ( const function_application_exprt &  expr, const namespacet &  ns  )

static

Simplify String.contains function when arguments are constant.

Definition at line 257 of file simplify_expr.cpp.

simplify_string_endswith()

static simplify_exprt::resultt simplify_string_endswith ( const function_application_exprt &  expr, const namespacet &  ns  )

static

Simplify String.endsWith function when arguments are constant.

Parameters

expr	the expression to simplify
ns	namespace

Returns

the modified expression or an unchanged expression

Definition at line 229 of file simplify_expr.cpp.

simplify_string_equals_ignore_case()

static simplify_exprt::resultt simplify_string_equals_ignore_case ( const function_application_exprt &  expr, const namespacet &  ns  )

static

Simplify String.equalsIgnorecase function when arguments are constant.

Parameters

expr	the expression to simplify
ns	namespace

Returns

: the modified expression or an unchanged expression

Definition at line 589 of file simplify_expr.cpp.

simplify_string_index_of()

static simplify_exprt::resultt simplify_string_index_of ( const function_application_exprt &  expr, const namespacet &  ns, const bool  search_from_end  )

static

Simplify String.indexOf function when arguments are constant.

Parameters

expr	the expression to simplify
ns	namespace
search_from_end	return the last instead of the first index

Returns

: the modified expression or an unchanged expression

Definition at line 376 of file simplify_expr.cpp.

simplify_string_is_empty()

static simplify_exprt::resultt simplify_string_is_empty ( const function_application_exprt &  expr, const namespacet &  ns  )

static

Simplify String.isEmpty function when arguments are constant.

Parameters

expr	the expression to simplify
ns	namespace

Returns

the modified expression or an unchanged expression

Definition at line 302 of file simplify_expr.cpp.

simplify_string_startswith()

static simplify_exprt::resultt simplify_string_startswith ( const function_application_exprt &  expr, const namespacet &  ns  )

static

Simplify String.startsWith function when arguments are constant.

Parameters

expr	the expression to simplify
ns	namespace

Returns

: the modified expression or an unchanged expression

Definition at line 634 of file simplify_expr.cpp.