why3/examples/mlcfg/basic.mlcfg

module Basic

use int.Int

let cfg cfgassert (x:int) : int
  requires { x >= 10 }
  ensures { result >= x }
  =
  {
  assert { x >= 0 };
  return x+1
  }


let cfg cfggoto (x:int) : int
  requires { x >= 0 }
  ensures { result = x + 2 }
  =
  var y : int;
  {
  y <- x+1;
  goto L
  }
  L {
  y <- y+1;
  return y
  }

let cfg cfg_inv (x:int) : int
  requires { x >= 0 }
  ensures { result >= 2 }
  =
  var y:int;
  {
  y <- x;
  invariant { y >= 0} ;
  y <- y + 1;
  invariant { y >= 1} ;
  y <- y + 1;
  return y
  }


let cfg cfg_infinite_loop (x:int) : int
  requires { x >= 0 }
  ensures { result >= 2 }
  =
  var y:int;
  {
  y <- 0;
  goto L
  }
  L {
  y <- y + 1;
  invariant { exists z. y = z+z+1 };
  y <- y + 1;
  goto L
  }


let cfg cfg_finite_loop (x:int) : int
  requires { x >= 0 }
  ensures { result >= 2 }
  =
  var y:int;
  {
  y <- 0;
  goto L
  }
  L {
  y <- y + 1;
  invariant { exists z. y = z+z+1 };
  y <- y + 1;
  switch (y <= x)
  | True -> goto L
  | False -> return y
  end
  }

let main () =
  let _ = cfgassert 42 in
  let _ = cfggoto 43 in
  let _ = cfg_inv 44 in
  ()

end