examples/mlcfg/basic.mlcfg

   1
   2 module Basic
   3
   4 use int.Int
   5
   6 let cfg cfgassert (x:int) : int
   7   requires { x >= 10 }
   8   ensures { result >= x }
   9   =
  10   {
  11   assert { x >= 0 };
  12   return x+1
  13   }
  14
  15
  16 let cfg cfggoto (x:int) : int
  17   requires { x >= 0 }
  18   ensures { result = x + 2 }
  19   =
  20   var y : int;
  21   {
  22   y <- x+1;
  23   goto L
  24   }
  25   L {
  26   y <- y+1;
  27   return y
  28   }
  29
  30 let cfg cfg_inv (x:int) : int
  31   requires { x >= 0 }
  32   ensures { result >= 2 }
  33   =
  34   var y:int;
  35   {
  36   y <- x;
  37   invariant { y >= 0} ;
  38   y <- y + 1;
  39   invariant { y >= 1} ;
  40   y <- y + 1;
  41   return y
  42   }
  43
  44
  45 let cfg cfg_infinite_loop (x:int) : int
  46   requires { x >= 0 }
  47   ensures { result >= 2 }
  48   =
  49   var y:int;
  50   {
  51   y <- 0;
  52   goto L
  53   }
  54   L {
  55   y <- y + 1;
  56   invariant { exists z. y = z+z+1 };
  57   y <- y + 1;
  58   goto L
  59   }
  60
  61
  62 let cfg cfg_finite_loop (x:int) : int
  63   requires { x >= 0 }
  64   ensures { result >= 2 }
  65   =
  66   var y:int;
  67   {
  68   y <- 0;
  69   goto L
  70   }
  71   L {
  72   y <- y + 1;
  73   invariant { exists z. y = z+z+1 };
  74   y <- y + 1;
  75   switch (y <= x)
  76   | True -> goto L
  77   | False -> return y
  78   end
  79   }
  80
  81 let main () =
  82   let _ = cfgassert 42 in
  83   let _ = cfggoto 43 in
  84   let _ = cfg_inv 44 in
  85   ()
  86
  87 end