Loading...

Searching...

No Matches

array_pool.h File Reference

Associates arrays and length to pointers, so that the string refinement can transform builtin function calls with pointer arguments to formulas over arrays. More...

#include <util/std_expr.h>
#include <util/string_expr.h>

+ Include dependency graph for array_pool.h:

[フレーム]

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

[フレーム]

Go to the source code of this file.

Classes

class symbol_generatort

Generation of fresh symbols of a given type. More...

class array_poolt

Correspondance between arrays and pointers string representations. More...

Functions

array_string_exprt of_argument (array_poolt &array_pool, const exprt &arg)

Converts a struct containing a length and pointer to an array.

array_string_exprt get_string_expr (array_poolt &array_pool, const exprt &expr)

Fetch the string_exprt corresponding to the given refined_string_exprt.

Detailed Description

Associates arrays and length to pointers, so that the string refinement can transform builtin function calls with pointer arguments to formulas over arrays.

Definition in file array_pool.h.

Function Documentation

◆ get_string_expr()

array_string_exprt get_string_expr ( array_poolt & array_pool,

const exprt & expr

)

Fetch the string_exprt corresponding to the given refined_string_exprt.

Parameters: array_pool pool of arrays representing strings

expr an expression of refined string type

Returns: a string expression

Definition at line 199 of file array_pool.cpp.

◆ of_argument()

array_string_exprt of_argument ( array_poolt & array_pool,

const exprt & arg

)

Converts a struct containing a length and pointer to an array.

This allows to get a string expression from arguments of a string builtion function, because string arguments in these function calls are given as a struct containing a length and pointer to an array.

Definition at line 193 of file array_pool.cpp.