@@ -80,7 +80,7 @@ class goto_checkt
80
80
protected:
81
81
const namespacet &ns;
82
82
std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
83
- goto_programt::const_targett t ;
83
+ goto_programt::const_targett current_target ;
84
84
85
85
void check_rec (
86
86
const exprt &expr,
@@ -289,11 +289,8 @@ void goto_checkt::undefined_shift_check(
289
289
if (width_expr.is_nil ())
290
290
throw " no number for width for operator " +expr.id_string ();
291
291
292
- binary_relation_exprt inequality (
293
- expr.distance (), ID_lt, width_expr);
294
-
295
292
add_guarded_claim (
296
- inequality ,
293
+ binary_relation_exprt (expr. distance (), ID_lt, width_expr) ,
297
294
" shift distance too large" ,
298
295
" undefined-shift" ,
299
296
expr.find_source_location (),
@@ -965,7 +962,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
965
962
const auto &pointer_type = to_pointer_type (address.type ());
966
963
967
964
local_bitvector_analysist::flagst flags =
968
- local_bitvector_analysis->get (t , address);
965
+ local_bitvector_analysis->get (current_target , address);
969
966
970
967
// For Java, we only need to check for null
971
968
if (mode == ID_java)
@@ -1535,7 +1532,7 @@ void goto_checkt::goto_check(
1535
1532
1536
1533
Forall_goto_program_instructions (it, goto_program)
1537
1534
{
1538
- t= it;
1535
+ current_target = it;
1539
1536
goto_programt::instructiont &i=*it;
1540
1537
1541
1538
new_code.clear ();
@@ -1606,8 +1603,8 @@ void goto_checkt::goto_check(
1606
1603
{
1607
1604
exprt pointer=code_function_call.arguments ()[0 ];
1608
1605
1609
- local_bitvector_analysist::flagst flags=
1610
- local_bitvector_analysis->get (t , pointer);
1606
+ local_bitvector_analysist::flagst flags =
1607
+ local_bitvector_analysis->get (current_target , pointer);
1611
1608
1612
1609
if (flags.is_unknown () || flags.is_null ())
1613
1610
{
0 commit comments