cprover
|
#include <util/optional.h>
Go to the source code of this file.
Functions | |
bool | simplify (exprt &expr, const namespacet &ns) |
exprt | simplify_expr (exprt src, const namespacet &ns) |
optionalt< std::reference_wrapper< const array_exprt > > | try_get_string_data_array (const exprt &content, const namespacet &ns) |
Get char sequence from content field of a refined string expression. More... | |
bool simplify | ( | exprt & | expr, |
const namespacet & | ns | ||
) |
Definition at line 2693 of file simplify_expr.cpp.
exprt simplify_expr | ( | exprt | src, |
const namespacet & | ns | ||
) |
Definition at line 2698 of file simplify_expr.cpp.
optionalt<std::reference_wrapper<const array_exprt> > try_get_string_data_array | ( | const exprt & | content, |
const namespacet & | ns | ||
) |
Get char sequence from content field of a refined string expression.
If content
is of the form &id[e]
, where id
is an array-typed symbol expression (and e
is any expression), return the value of the symbol id
(as given by the value
field of the symbol in the namespace ns
); otherwise return an empty optional.
content | content field of a refined string expression |
ns | namespace |
Definition at line 1837 of file simplify_expr.cpp.