7
7
8
8
\*******************************************************************/
9
9
10
- #include < stdexcept>
11
- #include < iostream>
12
-
13
10
#include < util/std_expr.h>
14
- #include < goto-programs/goto_functions.h>
15
11
#include < util/string_utils.h>
12
+ #include < goto-programs/goto_functions.h>
16
13
17
14
#include " unwind.h"
18
15
#include " loop_utils.h"
@@ -54,7 +51,7 @@ void parse_unwindset(const std::string &us, unwind_sett &unwind_set)
54
51
int loop_bound=std::stoi (bound);
55
52
56
53
if (loop_bound<-1 )
57
- throw std::invalid_argument ( " given unwind bound < -1" ) ;
54
+ throw " given unwind bound < -1" ;
58
55
59
56
unwind_set[func][loop_id]=loop_bound;
60
57
}
@@ -144,8 +141,6 @@ void goto_unwindt::unwind(
144
141
const unsigned k,
145
142
const unwind_strategyt unwind_strategy) const
146
143
{
147
- assert (k>=0 );
148
-
149
144
std::vector<goto_programt::targett> iteration_points;
150
145
unwind (goto_program, loop_head, loop_exit, k, unwind_strategy,
151
146
iteration_points);
@@ -171,13 +166,11 @@ void goto_unwindt::unwind(
171
166
const unwind_strategyt unwind_strategy,
172
167
std::vector<goto_programt::targett> &iteration_points) const
173
168
{
174
- assert (k>=0 );
175
169
assert (iteration_points.empty ());
176
170
assert (loop_head->location_number <loop_exit->location_number );
177
171
178
172
// rest program after unwound part
179
173
goto_programt rest_program;
180
- assert (rest_program.instructions .empty ());
181
174
182
175
if (unwind_strategy==PARTIAL)
183
176
{
@@ -286,8 +279,6 @@ void goto_unwindt::unwind(
286
279
}
287
280
else
288
281
{
289
- assert (k==0 );
290
-
291
282
// insert skip for loop body
292
283
293
284
goto_programt::targett t_skip=goto_program.insert_before (loop_head);
@@ -379,18 +370,18 @@ void goto_unwindt::unwind(
379
370
{
380
371
assert (k>=-1 );
381
372
382
- const irep_idt func=goto_program.instructions .begin ()->function ;
383
- assert (!func.empty ());
384
-
385
373
for (goto_programt::const_targett i_it=goto_program.instructions .begin ();
386
374
i_it!=goto_program.instructions .end (); i_it++)
387
375
{
388
376
if (!i_it->is_backwards_goto ())
389
377
continue ;
390
378
391
- unsigned loop_id=i_it->loop_number ;
379
+ const irep_idt func=i_it->function ;
380
+ assert (!func.empty ());
381
+
382
+ unsigned loop_number=i_it->loop_number ;
392
383
393
- int final_k=get_k (func, loop_id , k, unwind_set);
384
+ int final_k=get_k (func, loop_number , k, unwind_set);
394
385
395
386
if (final_k==-1 )
396
387
continue ;
0 commit comments