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. More...
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)
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. More...

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.