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 exprt | is_upper_case (const exprt &character) |
Expression which is true for uppercase characters of the Basic Latin and Latin-1 supplement of unicode. More... | |
static exprt | is_lower_case (const exprt &character) |
Expression which is true for lower_case characters of the Basic Latin and Latin-1 supplement of unicode. More... | |
|
static |
Definition at line 290 of file string_builtin_function.cpp.
|
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.
Expression which is true for lower_case characters of the Basic Latin and Latin-1 supplement of unicode.
Definition at line 353 of file string_builtin_function.cpp.
Expression which is true for uppercase characters of the Basic Latin and Latin-1 supplement of unicode.
Definition at line 320 of file string_builtin_function.cpp.
|
static |
Make a string from a constant array.
Definition at line 114 of file string_builtin_function.cpp.
|
static |
Definition at line 102 of file string_builtin_function.cpp.