cprover
|
#include <solvers/refinement/string_constraint_generator.h>
#include <util/prefix.h>
#include <util/string_constant.h>
#include <util/unicode.h>
Go to the source code of this file.
Functions | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
Generates string constraints for constant strings
Definition in file string_constraint_generator_constants.cpp.
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.
res | array of characters for the result |
sval | a string constant |
guard | condition under which the axiom should apply, true by default |
Definition at line 24 of file string_constraint_generator_constants.cpp.
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.
fresh_symbol | generator of fresh symbols |
res | string expression for the result |
arg | expression of type string typet |
guard | condition under which res should be equal to arg |
Definition at line 82 of file string_constraint_generator_constants.cpp.
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.
f | function application with arguments integer length and character pointer ptr . |
Definition at line 63 of file string_constraint_generator_constants.cpp.
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.
fresh_symbol | generator of fresh symbols |
f | function application with an argument which is a string literal that is a constant with a string value. |
array_pool | pool of arrays representing strings |
Definition at line 114 of file string_constraint_generator_constants.cpp.