Loading...

Searching...

No Matches

string_builtin_function.h File Reference

#include "string_constraint_generator.h"
#include <util/mathematical_expr.h>
#include <util/string_expr.h>
#include <vector>

+ Include dependency graph for string_builtin_function.h:

[フレーム]

+ This graph shows which files directly or indirectly include this file:

[フレーム]

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.

Macro Definition Documentation

◆ CHARACTER_FOR_UNKNOWN

#define CHARACTER_FOR_UNKNOWN '?'

Module: String solver Author: Diffblue Ltd.

Definition at line 14 of file string_builtin_function.h.

Function Documentation

◆ eval_string()

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.

◆ make_string()

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.