if_decision_branch.mlw 681 Bytes
Newer Older
1 2 3

module Main

4
  use int.Int
5 6 7

  type path_sel_type = { mutable sel_path : bool}

8
  val path_selector [@model_trace:TEMP_NAME]: path_sel_type
9 10 11 12 13 14

end


module Other

15 16
  use int.Int
  use Main
17

18
  let f (a : int)
19 20 21
    ensures {result = 5}
  =
    (* The counterexample should contain the node_id 5454 here but not 121 *)
22
    if (path_selector.sel_path <- (a = 1); ([@branch_id=5454] path_selector).sel_path) then
23 24
      5
    else
25
      begin path_selector.sel_path <- true;
26
      (* The counterexample should contain the node_id 121 but not 5454 *)
27
      if (path_selector.sel_path <- (a = 5); ([@branch_id=121] path_selector).sel_path) then
28 29 30
        15
      else
        22
31
      end
32

33
end