Loading...

Searching...

No Matches

string_dependencies.cpp File Reference

#include "string_dependencies.h"
#include "string_concatenation_builtin_function.h"
#include "string_format_builtin_function.h"
#include <unordered_set>
#include <util/expr_iterator.h>
#include <util/graph.h>
#include <util/ssa_expr.h>

+ Include dependency graph for string_dependencies.cpp:

[フレーム]

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.

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.

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)

std::optional< exprt > add_node (string_dependenciest &dependencies, const exprt &expr, array_poolt &array_pool, symbol_generatort &fresh_symbol)

When a sub-expression of expr 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.

Function Documentation

◆ add_dependency_to_string_subexprs()

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

)

static

Definition at line 135 of file string_dependencies.cpp.

◆ add_node()

std::optional< exprt > add_node ( string_dependenciest & dependencies,

const exprt & expr,

array_poolt & array_pool,

symbol_generatort & fresh_symbol

)

When a sub-expression of expr 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.

Parameters: dependencies graph to which we add the node

expr an expression which may contain a call to a string builtin_function.

array_pool array pool containing arrays corresponding to the string exprt arguments of the builtin_function call

fresh_symbol used to create new symbols for the return values of builtin functions

Returns: An expression in which function applications have been replaced by symbols corresponding to the return_value field of the associated builtin function. Or an empty optional when no function applications has been encountered

Definition at line 197 of file string_dependencies.cpp.

◆ for_each_atomic_string()

static void for_each_atomic_string ( const array_string_exprt & e,

const std::function< void(const array_string_exprt &)> f

)

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 105 of file string_dependencies.cpp.

◆ to_string_builtin_function()

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

)

static

Construct a string_builtin_functiont object from a function application.

Returns: a unique pointer to the created object

Definition at line 25 of file string_dependencies.cpp.