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