@@ -63,6 +63,11 @@ struct simplify_expr_cachet
63
63
simplify_expr_cachet simplify_expr_cache;
64
64
#endif
65
65
66
+ static optionalt<std::reference_wrapper<const array_exprt>>
67
+ try_get_string_data_array (
68
+ const refined_string_exprt &s,
69
+ const namespacet &ns);
70
+
66
71
simplify_exprt::resultt<> simplify_exprt::simplify_abs (const abs_exprt &expr)
67
72
{
68
73
if (expr.op ().is_constant ())
@@ -1818,8 +1823,20 @@ optionalt<std::string> simplify_exprt::expr2bits(
1818
1823
return {};
1819
1824
}
1820
1825
1821
- optionalt<std::reference_wrapper<const array_exprt>>
1822
- simplify_exprt::try_get_string_data_array (
1826
+ // / Get char sequence from refined string expression
1827
+ // /
1828
+ // / If `s.content()` is of the form `&id[e]`, where `id` is an array-typed
1829
+ // / symbol expression (and `e` is any expression), return the value of the
1830
+ // / symbol `id` (as given by the `value` field of the symbol in the namespace
1831
+ // / `ns`); otherwise return an empty optional.
1832
+ // /
1833
+ // / \param s: refined string expression
1834
+ // / \param ns: namespace
1835
+ // / \return array expression representing the char sequence which forms the
1836
+ // / content of the refined string expression, empty optional if the content
1837
+ // / cannot be determined
1838
+ static optionalt<std::reference_wrapper<const array_exprt>>
1839
+ try_get_string_data_array (
1823
1840
const refined_string_exprt &s,
1824
1841
const namespacet &ns)
1825
1842
{
0 commit comments