cprover
Loading...
Searching...
No Matches
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()

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 3357 of file simplify_expr.cpp.

◆ simplify_expr()

exprt simplify_expr ( exprt src,
const namespacet & ns )

Definition at line 3362 of file simplify_expr.cpp.

◆ simplify_string_char_at()

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
exprthe expression to simplify
nsnamespace
Returns
: the modified expression or an unchanged expression

Definition at line 521 of file simplify_expr.cpp.

◆ simplify_string_compare_to()

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
exprthe expression to simplify
nsnamespace
Returns
the modified expression or an unchanged expression

Definition at line 327 of file simplify_expr.cpp.

◆ simplify_string_contains()

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()

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

Simplify String.endsWith function when arguments are constant.

Parameters
exprthe expression to simplify
nsnamespace
Returns
the modified expression or an unchanged expression

Definition at line 229 of file simplify_expr.cpp.

◆ simplify_string_equals_ignore_case()

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
exprthe expression to simplify
nsnamespace
Returns
: the modified expression or an unchanged expression

Definition at line 589 of file simplify_expr.cpp.

◆ simplify_string_index_of()

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
exprthe expression to simplify
nsnamespace
search_from_endreturn 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()

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
exprthe expression to simplify
nsnamespace
Returns
the modified expression or an unchanged expression

Definition at line 302 of file simplify_expr.cpp.

◆ simplify_string_startswith()

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

Simplify String.startsWith function when arguments are constant.

Parameters
exprthe expression to simplify
nsnamespace
Returns
: the modified expression or an unchanged expression

Definition at line 634 of file simplify_expr.cpp.