Split exception examples into unit tests

Author: lyonel2017

config/tests.config

@@ -14,4 +14,4 @@ exclude = examples/MEE-CBC examples/old examples/old/list-ddh !examples/incomple
 okdirs = examples/MEE-CBC
 
 [test-unit]
-okdirs = tests
+okdirs = !tests

examples/exception.ec

@@ -0,0 +1,47 @@
+require import AllCore.
+
+abstract theory Et.
+  type t.
+
+  op test : t -> bool.
+
+  op truc : t -> exn.
+
+  exception et of t.
+  exception et2 of t * t.
+
+  print et2.
+
+  module Truc = {
+    proc f (x:t):t = {
+     if (test x) {raise (et x);}
+    return x;
+    }
+  }.
+
+  axiom hf :  forall (_x :t), hoare [Truc.f : _x = x ==> res = _x | et x => test x = false].
+end Et.
+
+require import List.
+
+exception et1 of int.
+
+clone Et as H with
+type t <- int.
+
+print H.
+print H.truc.
+print H.et.
+print H.et2.
+
+fail clone Et as H' with
+type t <- int,
+op et <- et1.
+
+clone Et as H' rename [exception] "et" as "ett".
+
+print H'.
+
+clone Et as H'' rename [op] "t" as "ett".
+
+print H''.

tests/exception/exception_abstract_theorie.ec

@@ -0,0 +1,25 @@
+require import AllCore.
+
+exception arg1 of int.
+
+op toto i = arg1 i.
+
+module M3 = {
+  proc f () = {
+    raise (toto 3);
+  }
+}.
+
+lemma test5 :
+  hoare [M3.f : true ==> false | arg1 x => x = 3].
+proof.
+  proc. wp. skip => //.
+qed.
+
+lemma test6 :
+  hoare [M3.f : true ==> false | arg1 x => x = 3].
+proof.
+  conseq (: _ ==> _ | arg1 x => 3 = x).
+  + done.
+  proc. wp. skip => //.
+qed.

tests/exception/exception_args.ec

@@ -0,0 +1,23 @@
+require import AllCore.
+
+(* exception arg ['a] of 'a. *)
+
+exception evar of int.
+
+op v : int.
+
+module Mv ={
+  var i:int
+
+  proc f1 (x:int) : int = {
+    i <- 0;
+    raise (evar (v + i)) ;
+    return x;
+  }
+}.
+
+lemma testv :
+  hoare [Mv.f1 : true ==> false | evar a => a = v].
+proof.
+  proc. wp. skip => //.
+qed.