2
Vote

Loop extraction bug

description

Original program:
procedure Main() returns(r:int)
{ 
  var i : int;
  var Flag : bool;
  var b : bool;
  i := 0;
  Flag := false;
  while(i<9)
  {
    havoc b;
    if (b || Flag) {
      i := i + 1; 
    }
    else {
     Flag := true;
    }
  }
}
Extracted program:
implementation Main_loop_anon4_LoopHead(in_i: int, in_Flag: bool, in_b: bool)
   returns (out_i: int, out_Flag: bool, out_b: bool)
{

  entry:
    out_i, out_Flag, out_b := in_i, in_Flag, in_b;
    goto anon4_LoopHead;

  anon4_LoopHead:
    goto anon4_LoopDone, anon4_LoopBody;

  anon4_LoopDone:
    assume {:partition} 9 <= out_i;
    out_i, out_Flag, out_b := in_i, in_Flag, in_b;
    return;

  anon5_Else:
    assume {:partition} !(out_b || out_Flag);
    out_Flag := true;
    goto anon5_Else_dummy;

  anon4_LoopBody:
    assume {:partition} out_i < 9;
    havoc out_b;
    goto anon5_Then, anon5_Else;

  anon5_Then:
    assume {:partition} out_b || out_Flag;
    out_i := out_i + 1;
    out_i, out_Flag, out_b := in_i, in_Flag, in_b;
    goto anon5_Then_dummy;

  anon5_Else_dummy:
    call {:si_unique_call 1} out_i, out_Flag, out_b := Main_loop_anon4_LoopHead(out_i, out_Flag, out_b);
    return;

  anon5_Then_dummy:
    call {:si_unique_call 2} out_i, out_Flag, out_b := Main_loop_anon4_LoopHead(out_i, out_Flag, out_b);
    return;

  exit:
    return;
}
Line: out_i, out_Flag, out_b := in_i, in_Flag, in_b; contains a bug.

comments