cprover
string_constraint_generatort Class Referencefinal

#include <string_constraint_generator.h>

+ Collaboration diagram for string_constraint_generatort:

Public Member Functions

 string_constraint_generatort (const namespacet &ns)
 
std::pair< exprt, string_constraintstadd_axioms_for_function_application (const function_application_exprt &expr)
 strings contained in this call are converted to objects of type string_exprt, through adding axioms. More...
 
optionalt< exprtmake_array_pointer_association (const function_application_exprt &expr)
 Associate array to pointer, and array to length. More...
 

Public Attributes

symbol_generatort fresh_symbol
 
array_poolt array_pool
 
string_constraintst constraints
 
const namespacet ns
 

Private Member Functions

exprt associate_array_to_pointer (const function_application_exprt &f)
 Associate a char array to a char pointer. More...
 
exprt associate_length_to_array (const function_application_exprt &f)
 Associate an integer length to a char array. More...
 

Private Attributes

const messaget message
 

Detailed Description

Definition at line 47 of file string_constraint_generator.h.

Constructor & Destructor Documentation

◆ string_constraint_generatort()

string_constraint_generatort::string_constraint_generatort ( const namespacet ns)
explicit

Definition at line 33 of file string_constraint_generator_main.cpp.

Member Function Documentation

◆ add_axioms_for_function_application()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_function_application ( const function_application_exprt expr)

strings contained in this call are converted to objects of type string_exprt, through adding axioms.

Axioms are then added to enforce that the result corresponds to the function application.

Parameters
expran expression containing a function application
Returns
expression corresponding to the result of the function application

Definition at line 219 of file string_constraint_generator_main.cpp.

◆ associate_array_to_pointer()

exprt string_constraint_generatort::associate_array_to_pointer ( const function_application_exprt f)
private

Associate a char array to a char pointer.

Insert in array_pool a binding from ptr to arr. If the length of arr is infinite, a new integer symbol is created and stored in array_pool. This also adds the default axioms for arr.

Parameters
fa function application with argument a character array arr and a character pointer ptr.

Definition at line 59 of file string_constraint_generator_main.cpp.

◆ associate_length_to_array()

exprt string_constraint_generatort::associate_length_to_array ( const function_application_exprt f)
private

Associate an integer length to a char array.

This adds an axiom ensuring that arr.length and length are equal.

Parameters
fa function application with argument a character array arr and an integer length.
Returns
integer expression equal to 0

Definition at line 81 of file string_constraint_generator_main.cpp.

◆ make_array_pointer_association()

optionalt< exprt > string_constraint_generatort::make_array_pointer_association ( const function_application_exprt expr)

Associate array to pointer, and array to length.

Returns
an expression if the given function application is one of associate pointer and associate length

Definition at line 202 of file string_constraint_generator_main.cpp.

Member Data Documentation

◆ array_pool

array_poolt string_constraint_generatort::array_pool

Definition at line 61 of file string_constraint_generator.h.

◆ constraints

string_constraintst string_constraint_generatort::constraints

Definition at line 63 of file string_constraint_generator.h.

◆ fresh_symbol

symbol_generatort string_constraint_generatort::fresh_symbol

Definition at line 59 of file string_constraint_generator.h.

◆ message

const messaget string_constraint_generatort::message
private

Definition at line 79 of file string_constraint_generator.h.

◆ ns

const namespacet string_constraint_generatort::ns

Definition at line 65 of file string_constraint_generator.h.


The documentation for this class was generated from the following files: