programs: fixed bug in WP for try/with

src/programs/pgm_typing.ml

@@ -1012,8 +1012,11 @@ and expr_desc gl env loc ty = function
 	in
 	x, v, expr gl env h
       in
-      let hl = List.map handler hl in
       let ef = List.fold_left (fun e (x,_,_) -> E.remove_raise x e) ef hl in
+      let hl = List.map handler hl in
+      let ef = 
+	List.fold_left (fun e (_,_,h) -> E.union e h.expr_effect) ef hl 
+      in
       Etry (e1, hl), tpure ty, ef
 
   | IEassert (k, f) ->

src/programs/pgm_typing.mli

@@ -24,3 +24,5 @@ val debug : Debug.flag
 val decl : 
   Env.env -> Pgm_env.env -> Pgm_ptree.decl -> Pgm_env.env * Pgm_ttree.decl list
 
+val print_post : Format.formatter -> Pgm_ttree.post -> unit
+

src/programs/pgm_wp.ml

@@ -197,7 +197,7 @@ let default_post ty ef =
   List.map default_exn_post (Sls.elements ef.E.raises)
 
 let rec assoc_handler x = function
-  | [] -> assert false
+  | [] -> raise Not_found
   | (y, h) :: _ when ls_equal x y -> h
   | _ :: hl -> assoc_handler x hl
 

tests/test-jcf.why

@@ -2,9 +2,9 @@
 (* test file *)
 
 theory Test
-  use import int.Int
-  logic (*) int int
-  goal G : not 1=2 and 3=4
+
+  type t = tuple2 int int
+
 end
 
 

tests/test-pgm-jcf.mlw

+exception Break
 
-{
-}
-
-let f x =
-  {}
-  if x = 1 then
-    1
-  else
-    if x = 2 then
-      2
-    else
-      3
-  {    x = 1
-    or (not x = 1 and x = 2)
-    or (not x = 1 and not x = 2 and result = 3) }
+let f (n : int) : int  =
+  { true }
+  let i = ref n in 
+  try
+    while (!i > 0) do
+      invariant { true }
+      variant { !i }
+      if (!i <= 10) then raise Break;
+      i := !i - 1
+    done
+  with Break -> ()
+  end;
+  !i
+  { result <= 10 } 
 
 (*
 Local Variables: