@@ -353,6 +353,48 @@ bool replace_malloc(
353
353
return result;
354
354
}
355
355
356
+ // / Replaces the RHS of the following instruction if it is an assignemnt
357
+ // / and its LHS is equal to name. Returns whether something was changed.
358
+ bool set_following_assign_to_true (
359
+ std::list<goto_programt::instructiont>::iterator it,
360
+ std::list<goto_programt::instructiont>::iterator end,
361
+ const std::string &name)
362
+ {
363
+ bool result=false ;
364
+ for (;it!=end;it++)
365
+ {
366
+ if (it->is_assign ())
367
+ {
368
+ code_assignt &code_assign=to_code_assign (it->code );
369
+ if (code_assign.lhs ().id ()==ID_symbol)
370
+ {
371
+ std::string lhs_id=
372
+ id2string (to_symbol_expr (code_assign.lhs ()).get_identifier ());
373
+ lhs_id=lhs_id.substr (0 , lhs_id.find (' #' , 0 ));
374
+ std::string var_name=name.substr (0 , name.find (' #' , 0 ));
375
+ if (lhs_id==var_name)
376
+ {
377
+ code_assign.rhs ()=true_exprt ();
378
+ result=true ;
379
+ }
380
+ }
381
+ }
382
+ if (it->is_dead ())
383
+ {
384
+ // Stop if the variable is invalid
385
+ code_deadt &code_dead=to_code_dead (it->code );
386
+ if (code_dead.symbol ().id ()==ID_symbol)
387
+ {
388
+ std::string dead_id=
389
+ id2string (to_symbol_expr (code_dead.symbol ()).get_identifier ());
390
+ if (name==dead_id)
391
+ break ;
392
+ }
393
+ }
394
+ }
395
+ return result;
396
+ }
397
+
356
398
// / Set undefined boolean variable to true. Finds declaration of a variable
357
399
// / whose name matches the given condition and adds an instruction var = TRUE
358
400
// / after the declaration.
@@ -375,6 +417,12 @@ void set_var_always_to_true(
375
417
id2string (to_symbol_expr (code_decl.symbol ()).get_identifier ());
376
418
if (name_cond (decl_id))
377
419
{
420
+ if (set_following_assign_to_true (
421
+ i_it,
422
+ f_it->second .body .instructions .end (),
423
+ decl_id))
424
+ continue ;
425
+ // No following assignment, add one
378
426
auto assign=f_it->second .body .insert_after (i_it);
379
427
assign->make_assignment ();
380
428
assign->code =code_assignt (code_decl.symbol (), true_exprt ());
0 commit comments