CBMC
|
#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"
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) |
|
static |
Take the passed-in constant string array and lower-case every character.
Definition at line 561 of file simplify_expr.cpp.
bool simplify | ( | exprt & | expr, |
const namespacet & | ns | ||
) |
Definition at line 3238 of file simplify_expr.cpp.
exprt simplify_expr | ( | exprt | src, |
const namespacet & | ns | ||
) |
Definition at line 3243 of file simplify_expr.cpp.
|
static |
Simplify String.charAt function when arguments are constant.
expr | the expression to simplify |
ns | namespace |
Definition at line 521 of file simplify_expr.cpp.
|
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
expr | the expression to simplify |
ns | namespace |
Definition at line 327 of file simplify_expr.cpp.
|
static |
Simplify String.contains function when arguments are constant.
Definition at line 257 of file simplify_expr.cpp.
|
static |
Simplify String.endsWith function when arguments are constant.
expr | the expression to simplify |
ns | namespace |
Definition at line 229 of file simplify_expr.cpp.
|
static |
Simplify String.equalsIgnorecase function when arguments are constant.
expr | the expression to simplify |
ns | namespace |
Definition at line 589 of file simplify_expr.cpp.
|
static |
Simplify String.indexOf function when arguments are constant.
expr | the expression to simplify |
ns | namespace |
search_from_end | return the last instead of the first index |
Definition at line 376 of file simplify_expr.cpp.
|
static |
Simplify String.isEmpty function when arguments are constant.
expr | the expression to simplify |
ns | namespace |
Definition at line 302 of file simplify_expr.cpp.
|
static |
Simplify String.startsWith function when arguments are constant.
expr | the expression to simplify |
ns | namespace |
Definition at line 634 of file simplify_expr.cpp.