programs: fixed typing related to exceptions which cannot be raised, or...

programs: fixed typing related to exceptions which cannot be raised, or possibly raised but no occuring in post (by the way: how should we issue warning in Why 3?)

examples/programs/next_digit_sum.mlw

@@ -22,7 +22,7 @@ let array_get (a : array 'a) i =
 let array_set (a : array 'a) i v = 
   { 0 <= i < A.length a } A.set a i v { result = A.set a i v }
 
-parameter x : array int
+parameter x : ref (array int)
 
 { 
   logic n : int
@@ -32,12 +32,23 @@ parameter x : array int
   use import int.EuclideanDivision
 
   logic m : int = 1 + max n (div y 9)
+
 }
 
+exception Success
+
 let search () =
-  { n >= 0 and y > 0 and A.length x >= m }
+  { n >= 0 and y > 0 and A.length !x >= m and
+    (n = 0 or !x#(n-1) <> 0) and
+    (forall i:int. 0 <= i < n -> 0 <= !x#i <= 9) and
+    (forall i:int. n <= i < m -> !x#i = 0) }
+  let s = ref 0 in
+  let i = ref 0 in
+  while !i < n do invariant { 0 <= !i <= n } (*variant { n - !i }*)
+    s := !s + array_get !x !i; i := !i + 1 
+  done;
   ()
-  { true }
+  { true(*false*) } (* | Success -> { true } *)
 
 (*
 Local Variables: 

src/programs/pgm_env.ml

@@ -93,6 +93,11 @@ let ls_Exit = memo_ls
 
 let v_result ty = create_vsymbol (id_fresh "result") ty
 
+let exn_v_result ls = match ls.ls_args with
+  | [] -> None
+  | [ty] -> Some (v_result ty)
+  | _ -> assert false
+
 let add_type_v_ref uc m =
   let ts_ref = find_ts uc ["ref"] in
   let a = ty_var (create_tvsymbol (id_fresh "a")) in

src/programs/pgm_env.mli

@@ -82,6 +82,7 @@ val apply_type_v_ref : env -> type_v -> reference -> type_c
 val occur_type_v : reference -> type_v -> bool
 
 val v_result : ty -> vsymbol
+val exn_v_result : Why.Term.lsymbol -> Why.Term.vsymbol option
 
 val post_map : (fmla -> fmla) -> post -> post
 

src/programs/pgm_typing.ml

@@ -887,6 +887,30 @@ let rec check_type ?(noref=false) gl loc ty = match ty.ty_node with
   | Ty.Tyvar _ -> 
       ()
 
+(* Saturation of postconditions: a postcondition must be set for
+   any possibly raised exception *)
+
+(* let warning_no_post loc x =  *)
+(*   wprintf loc "no postcondition for exception %a; false inserted@\n"  *)
+(*     Ident.print x; *)
+(*   if werror then exit 1 *)
+
+let saturation loc ef (a,al) =
+  let xs = ef.E.raises in
+  let check (x,_) =
+    if not (Sls.mem x xs) then 
+      errorm ~loc "exception %a cannot be raised" print_ls x
+  in
+  List.iter check al;
+  let set_post x = 
+    try 
+      x, List.assoc x al 
+    with Not_found -> 
+      (* warning_no_post loc x; *)
+      x, (exn_v_result x, f_false)
+  in
+  (a, List.map set_post (Sls.elements xs))
+
 (* [expr] translates iexpr into expr
    [env : type_v Mvs.t] maps local variables to their types *)
 
@@ -1030,6 +1054,7 @@ and expr_desc gl env loc ty = function
 
 and triple gl env (p, e, q) =
   let e = expr gl env e in
+  let q = saturation e.expr_loc e.expr_effect q in
   let ef = post_effect gl (fmla_effect gl e.expr_effect p) q in
   let e = { e with expr_effect = ef } in
   let c = 

src/programs/pgm_wp.ml

@@ -185,11 +185,6 @@ let rec ls_assoc ls = function
   | (ls', x) :: _ when ls_equal ls ls' -> x
   | _ :: r -> ls_assoc ls r
 
-let exn_v_result ls = match ls.ls_args with
-  | [] -> None
-  | [ty] -> Some (v_result ty)
-  | _ -> assert false
-
 let default_exn_post ls = ls, (exn_v_result ls, f_true)
 
 let default_post ty ef =