string_dependencies.h File Reference

Keeps track of dependencies between strings. More...

#include <memory>
#include "string_builtin_function.h"

Include dependency graph for string_dependencies.h:

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

Go to the source code of this file.

Classes
class	string_dependenciest
	Keep track of dependencies between strings. More...
class	string_dependenciest::builtin_function_nodet
	A builtin function node contains a builtin function call. More...
class	string_dependenciest::string_nodet
	A string node points to builtin_function on which it depends. More...
class	string_dependenciest::nodet
struct	string_dependenciest::node_hash
	Hash function for nodes. More...

Functions
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...

Detailed Description

Keeps track of dependencies between strings.

Definition in file string_dependencies.h.

Function Documentation

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.