@@ -16,6 +16,7 @@ Author: Daniel Poetzl
1616#include < goto-programs/remove_returns.h>
1717
1818#include < util/base_type.h>
19+ #include < util/exception_utils.h>
1920#include < util/invariant.h>
2021#include < util/irep.h>
2122#include < util/string_utils.h>
@@ -105,8 +106,9 @@ void replace_callst::operator()(
105106 if (rhs.id () == ID_symbol)
106107 {
107108 const symbol_exprt &se = to_symbol_expr (rhs);
108- if (has_suffix (id2string (se.get_identifier ()), RETURN_VALUE_SUFFIX))
109- throw " Returns must not be removed before replacing calls" ;
109+ INVARIANT (
110+ !has_suffix (id2string (se.get_identifier ()), RETURN_VALUE_SUFFIX),
111+ " returns must not be removed before replacing calls" );
110112 }
111113 }
112114
@@ -132,7 +134,10 @@ replace_callst::replacement_mapt replace_callst::parse_replacement_list(
132134 replacement_map.insert (std::make_pair (original, replacement));
133135
134136 if (!r.second )
135- throw " Conflicting replacement for function " + original;
137+ {
138+ throw invalid_user_input_exceptiont (
139+ " conflicting replacement for function " + original, " --replace-calls" );
140+ }
136141 }
137142
138143 return replacement_map;
@@ -146,22 +151,26 @@ void replace_callst::check_replacement_map(
146151 for (const auto &p : replacement_map)
147152 {
148153 if (replacement_map.find (p.second ) != replacement_map.end ())
149- throw " Function " + id2string (p.second ) +
150- " cannot both be replaced and "
151- " be a replacement" ;
154+ throw invalid_user_input_exceptiont (
155+ " function " + id2string (p.second ) +
156+ " cannot both be replaced and be a replacement" ,
157+ " --replace-calls" );
152158
153159 auto it2 = goto_functions.function_map .find (p.second );
154160
155161 if (it2 == goto_functions.function_map .end ())
156- throw " Replacement function " + id2string (p.second ) +
157- " needs to be present" ;
162+ throw invalid_user_input_exceptiont (
163+ " replacement function " + id2string (p.second ) + " needs to be present" ,
164+ " --replace-calls" );
158165
159166 auto it1 = goto_functions.function_map .find (p.first );
160167 if (it1 != goto_functions.function_map .end ())
161168 {
162169 if (!base_type_eq (it1->second .type , it2->second .type , ns))
163- throw " Functions " + id2string (p.first ) + " and " +
164- id2string (p.second ) + " are not type-compatible" ;
170+ throw invalid_user_input_exceptiont (
171+ " functions " + id2string (p.first ) + " and " + id2string (p.second ) +
172+ " are not type-compatible" ,
173+ " --replace-calls" );
165174 }
166175 }
167176}
0 commit comments