cprover
|
#include <algorithm>
#include <numeric>
#include <functional>
#include <iostream>
#include <util/arith_tools.h>
#include <util/expr_util.h>
#include <util/ssa_expr.h>
#include <util/std_expr.h>
#include <util/expr_iterator.h>
#include <util/graph.h>
#include <util/magic.h>
#include <util/make_unique.h>
#include <unordered_set>
#include "string_refinement_util.h"
Go to the source code of this file.
Functions | |
static void | for_each_atomic_string (const array_string_exprt &e, const std::function< void(const array_string_exprt &)> f) |
Applies f on all strings contained in e that are not if-expressions. More... | |
bool | is_char_type (const typet &type) |
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character. More... | |
bool | is_char_array_type (const typet &type, const namespacet &ns) |
Distinguish char array from other types. More... | |
bool | is_char_pointer_type (const typet &type) |
For now, any unsigned bitvector type is considered a character. More... | |
bool | has_char_pointer_subtype (const typet &type, const namespacet &ns) |
bool | has_char_array_subexpr (const exprt &expr, const namespacet &ns) |
static std::unique_ptr< string_builtin_functiont > | to_string_builtin_function (const function_application_exprt &fun_app, const exprt &return_code, array_poolt &array_pool) |
Construct a string_builtin_functiont object from a function application. More... | |
static void | add_dependency_to_string_subexprs (string_dependenciest &dependencies, const function_application_exprt &fun_app, const string_dependenciest::builtin_function_nodet &builtin_function_node, array_poolt &array_pool) |
bool | add_node (string_dependenciest &dependencies, const equal_exprt &equation, array_poolt &array_pool) |
When right hand side of equation is a builtin_function add a "string_builtin_function" node to the graph and connect it to the strings on which it depends and which depends on it. More... | |
|
static |
Definition at line 311 of file string_refinement_util.cpp.
bool add_node | ( | string_dependenciest & | dependencies, |
const equal_exprt & | equation, | ||
array_poolt & | array_pool | ||
) |
When right hand side of equation is a builtin_function add a "string_builtin_function" node to the graph and connect it to the strings on which it depends and which depends on it.
If the string builtin_function is not a supported one, mark all the string arguments as depending on an unknown builtin_function.
dependencies | graph to which we add the node |
equation | an equation whose right hand side is possibly a call to a string builtin_function. |
array_pool | array pool containing arrays corresponding to the string exprt arguments of the builtin_function call |
Definition at line 373 of file string_refinement_util.cpp.
|
static |
Applies f
on all strings contained in e
that are not if-expressions.
For instance on input cond1?s1:cond2?s2:s3
we apply f
on s1, s2 and s3.
Definition at line 281 of file string_refinement_util.cpp.
bool has_char_array_subexpr | ( | const exprt & | expr, |
const namespacet & | ns | ||
) |
expr | an expression |
ns | namespace |
expr
is an array of characters Definition at line 54 of file string_refinement_util.cpp.
bool has_char_pointer_subtype | ( | const typet & | type, |
const namespacet & | ns | ||
) |
type | a type |
ns | namespace |
type
is an pointer of characters. The meaning of "subtype" is in the algebraic datatype sense: for example, the subtypes of a struct are the types of its components, the subtype of a pointer is the type it points to, etc... Definition at line 49 of file string_refinement_util.cpp.
bool is_char_array_type | ( | const typet & | type, |
const namespacet & | ns | ||
) |
Distinguish char array from other types.
For now, any unsigned bitvector type is considered a character.
type | a type |
ns | namespace |
Definition at line 37 of file string_refinement_util.cpp.
bool is_char_pointer_type | ( | const typet & | type | ) |
For now, any unsigned bitvector type is considered a character.
type | a type |
Definition at line 44 of file string_refinement_util.cpp.
bool is_char_type | ( | const typet & | type | ) |
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.
type | a type |
Definition at line 30 of file string_refinement_util.cpp.
|
static |
Construct a string_builtin_functiont object from a function application.
Definition at line 206 of file string_refinement_util.cpp.