CBMC
Loading...
Searching...
No Matches
Functions
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 3407 of file simplify_expr.cpp.

◆  simplify_expr()

exprt simplify_expr ( exprt  src,
const namespacet &  ns 
)

Definition at line 3412 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.

AltStyle によって変換されたページ (->オリジナル) /