cprover
|
#include "string_builtin_function.h"
#include <algorithm>
#include <iterator>
#include "string_constraint_generator.h"
Go to the source code of this file.
Functions | |
static optionalt< std::vector< mp_integer > > | eval_string (const array_string_exprt &a, const std::function< exprt(const exprt &)> &get_value) |
Module: String solver Author: Diffblue Ltd. More... | |
static array_string_exprt | make_string (const std::vector< mp_integer > &array, const array_typet &array_type) |
Make a string from a constant array. More... | |
template<typename Iter > | |
static array_string_exprt | make_string (Iter begin, Iter end, const array_typet &array_type) |
static bool | eval_is_upper_case (const mp_integer &c) |
|
static |
Definition at line 192 of file string_builtin_function.cpp.
Referenced by string_to_lower_case_builtin_functiont::eval(), and string_to_upper_case_builtin_functiont::eval().
|
static |
Module: String solver Author: Diffblue Ltd.
Given a function get_value
which gives a valuation to expressions, attempt to find the current value of the array a
. If the valuation of some characters are missing, then return an empty optional.
Definition at line 67 of file string_builtin_function.cpp.
References if_exprt::cond(), array_string_exprt::content(), expr_try_dynamic_cast(), if_exprt::false_case(), irept::id(), exprt::is_constant(), exprt::is_true(), exprt::operands(), to_array_string_expr(), to_if_expr(), and if_exprt::true_case().
Referenced by string_concat_char_builtin_functiont::eval(), string_set_char_builtin_functiont::eval(), string_to_lower_case_builtin_functiont::eval(), string_to_upper_case_builtin_functiont::eval(), and string_insertion_builtin_functiont::eval().
|
static |
Make a string from a constant array.
Definition at line 114 of file string_builtin_function.cpp.
Referenced by string_concat_char_builtin_functiont::eval(), string_set_char_builtin_functiont::eval(), string_to_lower_case_builtin_functiont::eval(), string_to_upper_case_builtin_functiont::eval(), string_insertion_builtin_functiont::eval(), and string_of_int_builtin_functiont::eval().
|
static |
Definition at line 102 of file string_builtin_function.cpp.
References char_type(), from_integer(), exprt::operands(), typet::subtype(), and to_array_string_expr().