exercises Interproc

ex1: ————————————————————————————————

var x:int;
begin
  x=1;
  while x <= 100 do
   x=x+1;
  done;
  if (x<101 or x > 101) then fail;  endif;
end

Box: Annotated program after forward analysis
var x : int;
begin
  /* (L2 C5) top */
  x = 1; /* (L3 C6) [|x-1>=0; -x+101>=0|] */
  while x <= 100 do
    /* (L4 C19) [|x-1>=0; -x+100>=0|] */
    x = x + 1; /* (L5 C9)
                  [|x-2>=0; -x+101>=0|] */
  done; /* (L6 C7) [|x-101=0|] */
  if x < 101 or x > 101 then
    /* (L7 C28) bottom */
    fail; /* (L7 C34) bottom */
  endif; /* (L7 C42) [|x-101=0|] */
end

ex6: ————————————————————————————————

var x : int, y : int;
begin
  y = x; 
  if x > 0 then
    if y <= 0 then
      fail; 
    endif; 
  endif; 
end

Box: Annotated program after forward analysis
var x : int, y : int;
begin
  /* (L2 C5) top */
  y = x; /* (L3 C4) top */
  if x > 0 then
    /* (L4 C14) [|x-1>=0|] */
    if y <= 0 then
      /* (L5 C20) [|x-1>=0; -y>=0|] */
      fail; /* (L5 C26) bottom */
    endif; /* (L5 C33) [|x-1>=0; y-1>=0|] */
  endif; /* (L6 C6) top */
end

Octagon: Annotated program after forward analysis
var x : int, y : int;
begin
  /* (L2 C5) top */
  y = x; /* (L3 C4) [|-x+y>=0; x-y>=0|] */
  if x > 0 then
    /* (L4 C14)
       [|x-1>=0; -x+y>=0; x+y-2>=0; y-1>=0; x-y>=0|] */
    if y <= 0 then
      /* (L5 C20) bottom */
      fail; /* (L5 C26) bottom */
    endif; /* (L5 C33)
              [|x-1>=0; -x+y>=0; x+y-2>=0; y-1>=0; x-y>=0|] */
  endif; /* (L6 C6) [|-x+y>=0; x-y>=0|] */
end


ex8: ————————————————————————————————

var x:int, y:int;
begin
  x=0;
  while (x < 10 or x >10) do
    if brandom then
      x=x+3;
    else
      x=5*x-6*y;
   endif;
  done;
  fail;  
end

Convex polyhedra : Annotated program after forward analysis
var x : int, y : int;
begin
  /* (L3 C5) top */
  x = 0; /* (L4 C6) top */
  while x < 10 or x > 10 do
    /* (L5 C28) top */
    if brandom then
       /* (L6 C19) top */
       x = x + 3; /* (L7 C12) top */
    else
      /* (L8 C8) top */
      x = 5 * x - 6 * y; /* (L9 C16) top */
    endif; /* (L10 C9) top */
  done; /* (L11 C7) [|x-10=0|] */
  fail; /* (L12 C7) bottom */
end

Linear congruences: Annotated program after forward analysis
var x : int, y : int;
begin
  /* (L3 C5) [|y=0 mod 1; x=0 mod 1|] */
  x = 0; /* (L4 C6) [|3y=0 mod 3; x=0 mod 3|] */
  while x < 10 or x > 10 do
    /* (L5 C28) [|3y=0 mod 3; x=0 mod 3|] */
    if brandom then
       /* (L6 C19) [|3y=0 mod 3; x=0 mod 3|] */
       x = x + 3; /* (L7 C12)
                     [|3y=0 mod 3; x=0 mod 3|] */
    else
      /* (L8 C8) [|3y=0 mod 3; x=0 mod 3|] */
      x = 5 * x - 6 * y; /* (L9 C16)
                            [|-2x+3y=0 mod 15; 5x=0 mod 15|] */
    endif; /* (L10 C9)
              [|3y=0 mod 3; x=0 mod 3|] */
  done; /* (L11 C7) bottom */
  fail; /* (L12 C7) bottom */
end