Skip to content

Commit 7646cde

Browse files
committed
Factor out print_parse_tree function
This is currently implemented using `pretty`, but this function is used forward to replace with an implementation specific to our use case which is more easily readable by users of CBMC.
1 parent c4905f3 commit 7646cde

File tree

1 file changed

+13
-1
lines changed

1 file changed

+13
-1
lines changed

src/solvers/smt2_incremental/smt_response_validation.cpp

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -107,13 +107,25 @@ response_or_errort<smt_baset> validation_propagating(argumentst &&... arguments)
107107
}
108108
}
109109

110+
/// Produces a human-readable representation of the given \p parse_tree, for use
111+
/// in error messaging.
112+
/// \note This is currently implemented using `pretty`, but this function is
113+
/// used instead of calling `pretty` directly so that will be more straight
114+
/// forward to replace with an implementation specific to our use case which
115+
/// is more easily readable by users of CBMC.
116+
static std::string print_parse_tree(const irept &parse_tree)
117+
{
118+
return parse_tree.pretty(0, 0);
119+
}
120+
110121
static response_or_errort<irep_idt>
111122
validate_string_literal(const irept &parse_tree)
112123
{
113124
if(!parse_tree.get_sub().empty())
114125
{
115126
return response_or_errort<irep_idt>(
116-
"Expected string literal, found \"" + parse_tree.pretty(0, 0) + "\".");
127+
"Expected string literal, found \"" + print_parse_tree(parse_tree) +
128+
"\".");
117129
}
118130
return response_or_errort<irep_idt>{parse_tree.id()};
119131
}

0 commit comments

Comments
 (0)