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... | |
|
static |
Module: String solver Author: Diffblue Ltd.
Get the valuation of the string, given a valuation
Definition at line 92 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_transformation_builtin_functiont::eval(), and string_insertion_builtin_functiont::eval().
|
static |
Make a string from a constant array.
Definition at line 126 of file string_builtin_function.cpp.
References char_type(), from_integer(), exprt::operands(), typet::subtype(), and to_array_string_expr().
Referenced by string_transformation_builtin_functiont::eval(), and string_insertion_builtin_functiont::eval().