Skip to content

Commit 6c04eda

Browse files
committed
Make try_get_string_data_array() non-static
This is so the function can be called outside of simplify_expr.cpp.
1 parent f851118 commit 6c04eda

File tree

2 files changed

+21
-21
lines changed

2 files changed

+21
-21
lines changed

src/util/simplify_expr.cpp

Lines changed: 2 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -64,11 +64,6 @@ struct simplify_expr_cachet
6464
simplify_expr_cachet simplify_expr_cache;
6565
#endif
6666

67-
static optionalt<std::reference_wrapper<const array_exprt>>
68-
try_get_string_data_array(
69-
const refined_string_exprt &s,
70-
const namespacet &ns);
71-
7267
simplify_exprt::resultt<> simplify_exprt::simplify_abs(const abs_exprt &expr)
7368
{
7469
if(expr.op().is_constant())
@@ -1670,22 +1665,8 @@ optionalt<std::string> simplify_exprt::expr2bits(
16701665
return {};
16711666
}
16721667

1673-
/// Get char sequence from refined string expression
1674-
///
1675-
/// If `s.content()` is of the form `&id[e]`, where `id` is an array-typed
1676-
/// symbol expression (and `e` is any expression), return the value of the
1677-
/// symbol `id` (as given by the `value` field of the symbol in the namespace
1678-
/// `ns`); otherwise return an empty optional.
1679-
///
1680-
/// \param s: refined string expression
1681-
/// \param ns: namespace
1682-
/// \return array expression representing the char sequence which forms the
1683-
/// content of the refined string expression, empty optional if the content
1684-
/// cannot be determined
1685-
static optionalt<std::reference_wrapper<const array_exprt>>
1686-
try_get_string_data_array(
1687-
const refined_string_exprt &s,
1688-
const namespacet &ns)
1668+
optionalt<std::reference_wrapper<const array_exprt>>
1669+
try_get_string_data_array(const refined_string_exprt &s, const namespacet &ns)
16891670
{
16901671
if(s.content().id() != ID_address_of)
16911672
{

src/util/simplify_expr.h

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,12 @@ Author: Daniel Kroening, [email protected]
1010
#ifndef CPROVER_UTIL_SIMPLIFY_EXPR_H
1111
#define CPROVER_UTIL_SIMPLIFY_EXPR_H
1212

13+
class array_exprt;
1314
class exprt;
1415
class namespacet;
16+
class refined_string_exprt;
17+
18+
#include <util/optional.h>
1519

1620
//
1721
// simplify an expression
@@ -27,4 +31,19 @@ bool simplify(
2731
// this is the preferred interface
2832
exprt simplify_expr(exprt src, const namespacet &ns);
2933

34+
/// Get char sequence from refined string expression
35+
///
36+
/// If `s.content()` is of the form `&id[e]`, where `id` is an array-typed
37+
/// symbol expression (and `e` is any expression), return the value of the
38+
/// symbol `id` (as given by the `value` field of the symbol in the namespace
39+
/// `ns`); otherwise return an empty optional.
40+
///
41+
/// \param s: refined string expression
42+
/// \param ns: namespace
43+
/// \return array expression representing the char sequence which forms the
44+
/// content of the refined string expression, empty optional if the content
45+
/// cannot be determined
46+
optionalt<std::reference_wrapper<const array_exprt>>
47+
try_get_string_data_array(const refined_string_exprt &s, const namespacet &ns);
48+
3049
#endif // CPROVER_UTIL_SIMPLIFY_EXPR_H

0 commit comments

Comments
 (0)