cprover
|
#include "string_constraint_generator.h"
#include <util/mathematical_expr.h>
#include <util/string_expr.h>
#include <vector>
Go to the source code of this file.
Classes | |
class | string_builtin_functiont |
Base class for string functions that are built in the solver. More... | |
class | string_transformation_builtin_functiont |
String builtin_function transforming one string into another. More... | |
class | string_concat_char_builtin_functiont |
Adding a character at the end of a string. More... | |
class | string_set_char_builtin_functiont |
Setting a character at a particular position of a string. More... | |
class | string_to_lower_case_builtin_functiont |
Converting each uppercase character of Basic Latin and Latin-1 supplement to the corresponding lowercase character. More... | |
class | string_to_upper_case_builtin_functiont |
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding uppercase character. More... | |
class | string_creation_builtin_functiont |
String creation from other types. More... | |
class | string_of_int_builtin_functiont |
String creation from integer types. More... | |
class | string_test_builtin_functiont |
String test. More... | |
class | string_builtin_function_with_no_evalt |
Functions that are not yet supported in this class but are supported by string_constraint_generatort. More... |
Macros | |
#define | CHARACTER_FOR_UNKNOWN '?' |
Module: String solver Author: Diffblue Ltd. |
Functions | |
std::optional< std::vector< mp_integer > > | eval_string (const array_string_exprt &a, const std::function< exprt(const exprt &)> &get_value) |
Given a function get_value which gives a valuation to expressions, attempt to find the current value of the array a. | |
array_string_exprt | make_string (const std::vector< mp_integer > &array, const array_typet &array_type) |
Make a string from a constant array. |
#define CHARACTER_FOR_UNKNOWN '?' |
Module: String solver Author: Diffblue Ltd.
Definition at line 14 of file string_builtin_function.h.
std::optional< std::vector< mp_integer > > eval_string | ( | const array_string_exprt & | a, |
const std::function< exprt(const exprt &)> & | get_value ) |
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 24 of file string_builtin_function.cpp.
array_string_exprt make_string | ( | const std::vector< mp_integer > & | array, |
const array_typet & | array_type ) |
Make a string from a constant array.
Definition at line 71 of file string_builtin_function.cpp.