examples/mlcfg/nested_loops.mlcfg

   1 module NestedLoops
   2 use int.Int
   3 let cfg nested_loops  _x : () =
   4   var a : int;
   5   var b : int;
   6   var c : int;
   7   var d : int;
   8   {
   9     goto BB0
  10   }
  11   BB0 {
  12     switch (true)
  13     | True -> goto B
  14     | False -> goto A
  15     end
  16   }
  17   BB1 {
  18     invariant { true };
  19     switch (True)
  20     | True -> goto C
  21     | False -> goto D
  22     end
  23   }
  24   C {
  25     c <- c + 1;
  26     goto BB1
  27   }
  28   D {
  29     d <- d + 1;
  30     goto BB0
  31   }
  32   B {
  33     b <- b + 1;
  34     goto BB1
  35   }
  36   A {
  37     a <- a + 1;
  38     return ()
  39   }
  40 (*
  41   loop i {
  42     b
  43     loop j {
  44       c
  45     }
  46     d
  47   }
  48   a
  49 *)
  50 end