CBMC
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. More...
 
static simplify_exprt::resultt simplify_string_contains (const function_application_exprt &expr, const namespacet &ns)
 Simplify String.contains function when arguments are constant. More...
 
static simplify_exprt::resultt simplify_string_is_empty (const function_application_exprt &expr, const namespacet &ns)
 Simplify String.isEmpty function when arguments are constant. More...
 
static simplify_exprt::resultt simplify_string_compare_to (const function_application_exprt &expr, const namespacet &ns)
 Simplify String.compareTo function when arguments are constant. More...
 
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. More...
 
static simplify_exprt::resultt simplify_string_char_at (const function_application_exprt &expr, const namespacet &ns)
 Simplify String.charAt function when arguments are constant. More...
 
static bool lower_case_string_expression (array_exprt &string_data)
 Take the passed-in constant string array and lower-case every character. More...
 
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. More...
 
static simplify_exprt::resultt simplify_string_startswith (const function_application_exprt &expr, const namespacet &ns)
 Simplify String.startsWith function when arguments are constant. More...
 
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 3238 of file simplify_expr.cpp.

◆ simplify_expr()

exprt simplify_expr ( exprt  src,
const namespacet ns 
)

Definition at line 3243 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
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()

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

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

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

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

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

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

Definition at line 634 of file simplify_expr.cpp.