cprover
string_constraint_generator_constants.cpp File Reference

Generates string constraints for constant strings. More...

+ Include dependency graph for string_constraint_generator_constants.cpp:

Go to the source code of this file.

Functions

std::pair< exprt, string_constraintstadd_axioms_for_constant (const array_string_exprt &res, irep_idt sval, const exprt &guard)
 Add axioms ensuring that the provided string expression and constant are equal. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_empty_string (const function_application_exprt &f)
 Add axioms to say that the returned string expression is empty. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_cprover_string (symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &arg, const exprt &guard)
 Convert an expression of type string_typet to a string_exprt. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_literal (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 String corresponding to an internal cprover string. More...
 

Detailed Description

Generates string constraints for constant strings.

Definition in file string_constraint_generator_constants.cpp.

Function Documentation

◆ add_axioms_for_constant()

std::pair<exprt, string_constraintst> add_axioms_for_constant ( const array_string_exprt res,
irep_idt  sval,
const exprt guard 
)

Add axioms ensuring that the provided string expression and constant are equal.

Parameters
resarray of characters for the result
svala string constant
guardcondition under which the axiom should apply, true by default
Returns
integer expression equal to zero

Definition at line 24 of file string_constraint_generator_constants.cpp.

◆ add_axioms_for_cprover_string()

std::pair<exprt, string_constraintst> add_axioms_for_cprover_string ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const exprt arg,
const exprt guard 
)

Convert an expression of type string_typet to a string_exprt.

Parameters
fresh_symbolgenerator of fresh symbols
resstring expression for the result
argexpression of type string typet
guardcondition under which res should be equal to arg
Returns
0 if constraints were added, 1 if expression could not be handled and no constraint was added. Expression we can handle are of the form \( e := "<string constant>" | (expr)? e : e \)

Definition at line 82 of file string_constraint_generator_constants.cpp.

◆ add_axioms_for_empty_string()

std::pair<exprt, string_constraintst> add_axioms_for_empty_string ( const function_application_exprt f)

Add axioms to say that the returned string expression is empty.

Parameters
ffunction application with arguments integer length and character pointer ptr.
Returns
integer expression equal to zero

Definition at line 63 of file string_constraint_generator_constants.cpp.

◆ add_axioms_from_literal()

std::pair<exprt, string_constraintst> add_axioms_from_literal ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

String corresponding to an internal cprover string.

Add axioms ensuring that the returned string expression is equal to the string literal.

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with an argument which is a string literal that is a constant with a string value.
array_poolpool of arrays representing strings
Returns
string expression

Definition at line 114 of file string_constraint_generator_constants.cpp.