better modularisation

src/plugins/e-acsl/Makefile.in

@@ -33,7 +33,17 @@ PLUGIN_DIR ?=.
 PLUGIN_ENABLE:=@ENABLE_E_ACSL@
 PLUGIN_DYNAMIC:=@DYNAMIC_E_ACSL@
 PLUGIN_NAME:=E_ACSL
-PLUGIN_CMO:= local_config options read_header error misc mpz env visit main
+PLUGIN_CMO:= local_config \
+	options \
+	read_header \
+	error \
+	misc \
+	mpz \
+	env \
+	typing \
+	quantif \
+	visit \
+	main
 PLUGIN_HAS_MLI:=yes
 
 # Enable -warn-error, but do not distribute the plug-in with this option being

src/plugins/e-acsl/TODO

@@ -66,7 +66,7 @@
 - test sizeof.i devraient être plus précis quand logic_typing plus précis
 - structs
 - unions
-- quantifications entières invalides
+- inclure exemple du E-ACSL Reference Manual
 
 ####################
 # AVANT LA DISTRIB #

src/plugins/e-acsl/quantif.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*                                                                        *)
+(*  Copyright (C) 2011                                                    *)
+(*    CEA (Commissariat  l'nergie atomique et aux nergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+open Cil
+open Cil_datatype
+
+let named_predicate_to_exp_ref
+    : (Env.t -> predicate named -> exp * Env.t) ref
+    = Extlib.mk_fun "named_predicate_to_exp_ref"
+
+let term_to_exp_ref
+    : (Env.t -> logic_type -> term -> exp * Env.t) ref
+    = Extlib.mk_fun "term_to_exp_ref"
+
+let compute_quantif_guards quantif bounded_vars hyps = 
+  let error msg pp x =
+    let msg1 = Pretty_utils.sfprintf msg pp x in
+    let msg2 = 
+      Pretty_utils.sfprintf "@[ in quantification@ %a@]"
+	d_predicate_named quantif
+    in
+    Error.untypable (msg1 ^ msg2)
+  in
+  let rec aux acc vars p = 
+    match p.content with
+    | Pand({ content = Prel((Rlt | Rle) as r1, t11, t12) },
+	   { content = Prel((Rlt | Rle) as r2, t21, t22) }) ->
+      (match t12.term_node, t21.term_node with
+      | TLval(TVar x1, TNoOffset), TLval(TVar x2, TNoOffset) -> 
+	let v, vars = match vars with
+	  | [] -> error "@[too much constraint(s)%a@]" (fun _ () -> ()) ()
+	  | v :: tl -> 
+	    match v.lv_type with
+	    | Ctype ty when isIntegralType ty -> v, tl
+	    | Linteger -> v, tl
+	    | Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ -> 
+	      error "@[non integer variable %a@]" d_logic_var v
+	in
+	if Logic_var.equal x1 x2 && Logic_var.equal x1 v then
+	  (t11, r1, x1, r2, t22) :: acc, vars
+	else
+	  error "@[invalid binder %a@]" d_term t21
+      | TLval _, _ -> error "@[invalid binder %a@]" d_term t21
+      | _, _ -> error "@[invalid binder %a@]" d_term t12)
+    | Pand(p1, p2) -> 
+      let acc, vars = aux acc vars p1 in
+      aux acc vars p2
+    | _ -> error "@[invalid guard %a@]" d_predicate_named p
+  in 
+  let acc, vars = aux [] bounded_vars hyps in
+  (match vars with
+  | [] -> ()
+  | _ :: _ ->
+    let msg = 
+      Pretty_utils.sfprintf
+	"@[unguarded variable%s %tin quantification@ %a@]" 
+	(if List.length vars = 1 then "" else "s") 
+	(fun fmt -> 
+	  List.iter (fun v -> Format.fprintf fmt "@[%a @]" d_logic_var v) vars)
+	d_predicate_named quantif
+    in
+    Error.untypable msg);
+  List.rev acc
+
+module Label_ids = 
+  State_builder.Counter(struct let name = "E_ACSL.Label_ids" end)
+
+let convert env loc p bounded_vars hyps goal =
+  let named_predicate_to_exp = !named_predicate_to_exp_ref in
+  let term_to_exp = !term_to_exp_ref in
+  (* universal quantification over integers (or a subtype of integer) *)
+  let guards = compute_quantif_guards p bounded_vars hyps in
+  let env = List.fold_left Env.Logic_binding.add env bounded_vars in
+  let var_res = ref Varinfo.dummy in
+  let res, env =
+    (* variable storing the result of the \forall *)
+    Env.new_var env None intType
+      (fun v _ ->
+	var_res := v;
+	let lv = var v in
+	[ mkStmtOneInstr ~valid_sid:true (Set(lv, one ~loc, loc)) ])
+  in
+  let end_loop_ref = ref dummyStmt in
+  let rec mk_for_loop env = function
+    | [] -> 
+      (* innermost loop body: store the result in [res] and go out according
+	 to evaluation of the goal *)
+      let test, env = named_predicate_to_exp (Env.push env) goal in
+      let then_block = mkBlock [ mkEmptyStmt ~loc () ] in
+      let else_block = 
+	(* use a 'goto', not a simple 'break' in order to handle 'forall' with
+	   multiple binders (leading to imbricated loops) *)
+	mkBlock
+	  [ mkStmtOneInstr
+	      ~valid_sid:true (Set(var !var_res, zero ~loc, loc));
+	    mkStmt ~valid_sid:true (Goto(end_loop_ref, loc)) ]
+      in
+      let blk, env = 
+	Env.pop_and_get
+	  env
+	  (mkStmt ~valid_sid:true (If(test, then_block, else_block, loc)))
+	  ~global_clear:false
+	  Env.After
+      in
+      (* TODO: could be optimised if [pop_and_get] would return a list of
+	 stmts *)
+      [ mkStmt ~valid_sid:true (Block blk) ], env
+    | (t1, rel1, logic_x, rel2, t2) :: tl ->
+      let body, env = mk_for_loop env tl in
+      let t_plus_one t =
+	Logic_const.term ~loc
+	  (TBinOp(PlusA, t, Logic_const.tinteger ~loc ~ikind:IChar 1))
+	  Linteger
+      in
+      let t1 = match rel1 with
+	| Rlt -> t_plus_one t1
+	| Rle -> t1
+	| Rgt | Rge | Req | Rneq -> assert false
+      in
+      let bop2 = match rel2 with
+	| Rlt -> Lt
+	| Rle -> Le
+	| Rgt | Rge | Req | Rneq -> assert false
+      in
+      (* we increment the loop counter one more time (at the end of the
+	 loop). Thus to prevent  overflow, check the type of [t2 + 1] instead
+	 of [t2]. *) 
+      let ty = Typing.principal_type_from_term t1 (t_plus_one t2) in
+      let ty = Typing.principal_type ty logic_x.lv_type in
+      (* loop counter corresponding to the quantified variable *)
+      let var_x = Env.Logic_binding.get env logic_x in
+      let lv_x = var var_x in
+      let x = new_exp ~loc (Lval lv_x) in
+      let env = match ty with
+	| Ctype ty when isIntegralType ty -> 
+	  var_x.vtype <- ty;
+	  env
+	| Linteger -> 
+	  var_x.vtype <- Mpz.t;
+	  Env.add_stmt env (Mpz.init x)
+	| Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ -> assert false
+      in
+      (* initialize the loop counter to [t1] *)
+      let e1, env = term_to_exp (Env.push env) ty t1 in
+      let init_blk, env = 
+	Env.pop_and_get 
+	  env
+	  (Mpz.affect lv_x x e1)
+	  ~global_clear:false
+	  Env.Middle
+      in
+      (* generate the guard [x bop t2] *)
+      let stmts_block b = [ mkStmt ~valid_sid:true (Block b) ] in
+      let tlv = Logic_const.tvar ~loc (cvar_to_lvar var_x) in
+      let guard_exp, env = 
+	term_to_exp
+	  (Env.push env)
+	  (Ctype intType)
+	  (Logic_const.term (TBinOp(bop2, tlv, t2)) ty)
+      in
+      let break_stmt = mkStmt ~valid_sid:true (Break guard_exp.eloc) in
+      let guard_blk, env =
+	Env.pop_and_get
+	  env
+	  (mkStmt ~valid_sid:true
+	     (If(guard_exp,
+		 mkBlock [ mkEmptyStmt () ],
+		 mkBlock [ break_stmt ], 
+		 guard_exp.eloc)))
+	  ~global_clear:false
+	  Env.Middle
+      in
+      let guard = stmts_block guard_blk in
+      (* increment the loop counter [x++] *)
+      let incr, env = term_to_exp (Env.push env) ty (t_plus_one tlv) in
+      let next_blk, env = 
+	Env.pop_and_get
+	  env
+	  (Mpz.affect lv_x x incr)
+	  ~global_clear:false
+	  Env.Middle
+      in
+      (* generate the whole loop *)
+      let start = stmts_block init_blk in
+      let next = stmts_block next_blk in
+      start @
+	[ mkStmt ~valid_sid:true
+	    (Loop ([],
+		   mkBlock (guard @ body @ next),
+		   loc, 
+		   None, 
+		   Some break_stmt)) ], 
+      env
+  in
+  let stmts, env = mk_for_loop env guards in
+  let env = 
+    Env.add_stmt env (mkStmt ~valid_sid:true (Block (mkBlock stmts))) 
+  in
+  (* where to jump to go out of the loop *)
+  let end_loop = mkEmptyStmt ~loc () in
+  let label_name = "e_acsl_end_loop" ^ string_of_int (Label_ids.next ()) in
+  let label = Label(label_name, loc, false) in
+  end_loop.labels <- label :: end_loop.labels;
+  end_loop_ref := end_loop;
+  let env = Env.add_stmt env end_loop in
+  let env = List.fold_left Env.Logic_binding.remove env bounded_vars in
+  res, env
+
+(*
+Local Variables:
+compile-command: "make"
+End:
+*)

src/plugins/e-acsl/quantif.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*                                                                        *)
+(*  Copyright (C) 2011                                                    *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+val convert: 
+  Env.t -> 
+  location ->
+  predicate named -> 
+  logic_var list -> 
+  predicate named -> 
+  predicate named -> 
+  exp * Env.t
+
+val named_predicate_to_exp_ref: (Env.t -> predicate named -> exp * Env.t) ref
+val term_to_exp_ref: (Env.t -> logic_type -> term -> exp * Env.t) ref
+
+(*
+Local Variables:
+compile-command: "make"
+End:
+*)

src/plugins/e-acsl/typing.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*                                                                        *)
+(*  Copyright (C) 2011                                                    *)
+(*    CEA (Commissariat  l'nergie atomique et aux nergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+open Cil
+
+let compatible_type ty ty' = 
+  (* compatible if the two type has the same "integrality" *)
+  isIntegralType ty = isIntegralType ty'
+
+(* convert [e] corresponding to a term of type [ty] in a way that it is
+   compatible with the given context. *)
+let context_sensitive ?loc env ctx is_mpz_string t_opt e = 
+  let ty = typeOf e in
+  let mk_mpz env e = 
+    Env.new_var env t_opt Mpz.t (fun lv v -> [ Mpz.init_set (var lv) v e ]) 
+  in
+  let do_int_ctx ty' =
+    let e, env = if is_mpz_string then mk_mpz env e else e, env in
+    if Mpz.is_t ty || is_mpz_string then
+      (* cast the mpz into a C integer *)
+      let name = 
+	if isSignedInteger ty' then "__gmpz_get_si" else "__gmpz_get_ui" 
+      in
+      Options.warning
+	?source:(Extlib.opt_map fst loc)
+	~once:true
+	"@[missing guard for ensuring that the given integer is \
+C-representable@]"; 
+      Env.new_var 
+	env
+	None
+	ty'
+	(fun v _ -> [ Misc.mk_call ?loc ~result:(var v) name [ e ] ])
+    else
+      e, env
+  in
+  match ctx with
+  | Ctype ty' -> do_int_ctx ty'
+  | Linteger ->
+    if Mpz.is_t ty then
+      e, env
+    else begin
+      (* Convert the C integer into a mpz. 
+	 Remember: very long integer constant has been temporary converted into
+	 strings *)
+      assert (Options.verify
+		(isIntegralType ty || is_mpz_string) 
+		"how to convert %a to an integer?"
+		d_type ty); 
+      mk_mpz env e
+    end
+  | ty' when Logic_const.is_boolean_type ty' -> do_int_ctx intType
+  | Ltype _ | Lvar _ | Lreal | Larrow _ -> 
+    (* not yet supported, thus cannot occur at this point *)
+    assert false
+
+let principal_type ty ty' = match ty, ty' with
+  | Ctype ty, Ctype ty' when isIntegralType ty -> 
+    assert (isIntegralType ty');
+    Ctype (arithmeticConversion ty ty')
+  | Ctype ty, Linteger | Linteger, Ctype ty when isIntegralType ty -> Linteger
+  (* not possible to unify cases below (see caml bts #5432) *)
+  | Ctype ty1, Ctype ty2 when Mpz.is_t ty1 && isIntegralType ty2 -> Linteger
+  | Ctype ty2, Ctype ty1 when Mpz.is_t ty1 && isIntegralType ty2 -> Linteger
+  | Ctype tty, Ctype tty' -> 
+    assert (compatible_type tty tty');
+    ty
+  | Ctype _, Linteger | Linteger, Ctype _ -> Linteger
+  | Linteger, Linteger -> Linteger
+  | (Ltype _ | Lvar _ | Lreal | Larrow _), _
+  | _, (Ltype _ | Lvar _ | Lreal | Larrow _) -> 
+    (* not yet supported, thus cannot occur at this point *)
+    Options.error "What is this %a here?" d_logic_type ty'; 
+    assert false
+
+let principal_type_from_term t1 t2 =
+  let typ t = 
+    let ty = t.term_type in
+    if Logic_const.is_boolean_type ty then Ctype intType
+    else match t.term_node, ty with
+    | TConst (CInt64(_, (ILongLong | IULongLong), _)), Linteger -> 
+      (* constant potentially not representable in C *)
+      Linteger
+    | TConst (CInt64(_, k, _)), _ -> 
+      (* C-representable constant *)
+      Ctype (TInt (k, []))
+    | _, _ -> 
+      (* for direct C terms, should be able to infer the corresponding C type *)
+      ty
+  in
+  principal_type (typ t1) (typ t2) 
+
+(*
+Local Variables:
+compile-command: "make"
+End:
+*)

src/plugins/e-acsl/typing.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the E-ACSL plug-in of Frama-C.                   *)
+(*                                                                        *)
+(*  Copyright (C) 2011                                                    *)
+(*    CEA (Commissariat  l'nergie atomique et aux nergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+(** Typing rules. *)
+
+val principal_type: logic_type -> logic_type -> logic_type
+val principal_type_from_term: term -> term -> logic_type
+
+val context_sensitive: 
+  ?loc:location -> Env.t -> logic_type -> bool -> term option -> exp -> 
+  exp * Env.t
+
+(*
+Local Variables:
+compile-command: "make"
+End:
+*)

src/plugins/e-acsl/visit.ml

@@ -24,98 +24,6 @@ open Cil_types
 open Cil_datatype
 open Cil
 
-(* ************************************************************************** *)
-(* Typing rules *)
-(* ************************************************************************** *)
-
-let compatible_type ty ty' = 
-  (* compatible if the two type has the same "integrality" *)
-  isIntegralType ty = isIntegralType ty'
-
-(* convert [e] corresponding to a term of type [ty] in a way that it is
-   compatible with the given context. *)
-let context_sensitive ?loc env ctx is_mpz_string t_opt e = 
-  let ty = typeOf e in
-  let mk_mpz env e = 
-    Env.new_var env t_opt Mpz.t (fun lv v -> [ Mpz.init_set (var lv) v e ]) 
-  in
-  let do_int_ctx ty' =
-    let e, env = if is_mpz_string then mk_mpz env e else e, env in
-    if Mpz.is_t ty || is_mpz_string then
-      (* cast the mpz into a C integer *)
-      let name = 
-	if isSignedInteger ty' then "__gmpz_get_si" else "__gmpz_get_ui" 
-      in
-      Options.warning
-	?source:(Extlib.opt_map fst loc)
-	~once:true
-	"@[missing guard for ensuring that the given integer is \
-C-representable@]"; 
-      Env.new_var 
-	env
-	None
-	ty'
-	(fun v _ -> [ Misc.mk_call ?loc ~result:(var v) name [ e ] ])
-    else
-      e, env
-  in
-  match ctx with
-  | Ctype ty' -> do_int_ctx ty'
-  | Linteger ->
-    if Mpz.is_t ty then
-      e, env
-    else begin
-      (* Convert the C integer into a mpz. 
-	 Remember: very long integer constant has been temporary converted into
-	 strings *)
-      assert (Options.verify
-		(isIntegralType ty || is_mpz_string) 
-		"how to convert %a to an integer?"
-		d_type ty); 
-      mk_mpz env e
-    end
-  | ty' when Logic_const.is_boolean_type ty' -> do_int_ctx intType
-  | Ltype _ | Lvar _ | Lreal | Larrow _ -> 
-    (* not yet supported, thus cannot occur at this point *)
-    assert false
-
-let principal_type ty ty' = match ty, ty' with
-  | Ctype ty, Ctype ty' when isIntegralType ty -> 
-    assert (isIntegralType ty');
-    Ctype (arithmeticConversion ty ty')
-  | Ctype ty, Linteger | Linteger, Ctype ty when isIntegralType ty -> Linteger
-  (* both cases below should be unified, but it is not possible because of
-     caml bts #5432 *)
-  | Ctype ty1, Ctype ty2 when Mpz.is_t ty1 && isIntegralType ty2 -> Linteger
-  | Ctype ty2, Ctype ty1 when Mpz.is_t ty1 && isIntegralType ty2 -> Linteger
-  | Ctype tty, Ctype tty' -> 
-    assert (compatible_type tty tty');
-    ty
-  | Ctype _, Linteger | Linteger, Ctype _ -> Linteger
-  | Linteger, Linteger -> Linteger
-  | (Ltype _ | Lvar _ | Lreal | Larrow _), _
-  | _, (Ltype _ | Lvar _ | Lreal | Larrow _) -> 
-    (* not yet supported, thus cannot occur at this point *)
-    Options.error "What is this %a here?" d_logic_type ty'; 
-    assert false
-
-let principal_type_from_term t1 t2 =
-  let typ t = 
-    let ty = t.term_type in
-    if Logic_const.is_boolean_type ty then Ctype intType
-    else match t.term_node, ty with
-    | TConst (CInt64(_, (ILongLong | IULongLong), _)), Linteger -> 
-      (* constant potentially not representable in C *)
-      Linteger
-    | TConst (CInt64(_, k, _)), _ -> 
-      (* C-representable constant *)
-      Ctype (TInt (k, []))
-    | _, _ -> 
-      (* for direct C terms, should be able to infer the corresponding C type *)
-      ty
-  in
-  principal_type (typ t1) (typ t2) 
-
 (* ************************************************************************** *)
 (* Transforming terms and predicates into C expressions (if any) *)
 (* ************************************************************************** *)
@@ -144,60 +52,6 @@ let is_representable _n k _s = match k with
   | ILongLong | IULongLong ->
     false
 
-let compute_quantif_guards quantif bounded_vars hyps = 
-  let error msg pp x =
-    let msg1 = Pretty_utils.sfprintf msg pp x in
-    let msg2 = 
-      Pretty_utils.sfprintf "@[ in quantification@ %a@]"
-	d_predicate_named quantif
-    in
-    Error.untypable (msg1 ^ msg2)
-  in
-  let rec aux acc vars p = 
-    match p.content with
-    | Pand({ content = Prel((Rlt | Rle) as r1, t11, t12) },
-	   { content = Prel((Rlt | Rle) as r2, t21, t22) }) ->
-      (match t12.term_node, t21.term_node with
-      | TLval(TVar x1, TNoOffset), TLval(TVar x2, TNoOffset) -> 
-	let v, vars = match vars with
-	  | [] -> error "@[too much constraint(s)%a@]" (fun _ () -> ()) ()
-	  | v :: tl -> 
-	    match v.lv_type with
-	    | Ctype ty when isIntegralType ty -> v, tl
-	    | Linteger -> v, tl
-	    | Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ -> 
-	      error "@[non integer variable %a@]" d_logic_var v
-	in
-	if Logic_var.equal x1 x2 && Logic_var.equal x1 v then
-	  (t11, r1, x1, r2, t22) :: acc, vars
-	else
-	  error "@[invalid binder %a@]" d_term t21
-      | TLval _, _ -> error "@[invalid binder %a@]" d_term t21
-      | _, _ -> error "@[invalid binder %a@]" d_term t12)
-    | Pand(p1, p2) -> 
-      let acc, vars = aux acc vars p1 in
-      aux acc vars p2
-    | _ -> error "@[invalid guard %a@]" d_predicate_named p
-  in 
-  let acc, vars = aux [] bounded_vars hyps in
-  (match vars with
-  | [] -> ()
-  | _ :: _ ->
-    let msg = 
-      Pretty_utils.sfprintf
-	"@[unguarded variable%s %tin quantification@ %a@]" 
-	(if List.length vars = 1 then "" else "s") 
-	(fun fmt -> 
-	  List.iter (fun v -> Format.fprintf fmt "@[%a @]" d_logic_var v) vars)
-	d_predicate_named quantif
-    in
-    Error.untypable msg);
-  List.rev acc
-
-
-module Label_ids = 
-  State_builder.Counter(struct let name = "E_ACSL.Label_ids" end)
-
 let constant_to_exp ?(loc=Location.unknown) = function
   | CInt64(n, k, s) ->
     if is_representable n k s then kinteger64_repr ?loc k n s, false
@@ -301,7 +155,7 @@ and context_insensitive_term_to_exp env t =
     e, env, false
   | TBinOp(Div | Mod as bop, t1, t2) ->
     (* arithmetic binary operator potentially convertible into C *)
-    let ctx = principal_type_from_term t1 t2 in
+    let ctx = Typing.principal_type_from_term t1 t2 in
     let e1, env = term_to_exp env ctx t1 in
     let e2, env = term_to_exp env ctx t2 in
     (* guarding divisions and modulos *)
@@ -438,22 +292,23 @@ and context_insensitive_term_to_exp env t =
    constructs. *)
 and term_to_exp env ctx t = 
   let e, env, is_mpz_string = context_insensitive_term_to_exp env t in
-  context_sensitive ~loc:t.term_loc env ctx is_mpz_string (Some t) e
+  Typing.context_sensitive ~loc:t.term_loc env ctx is_mpz_string (Some t) e
 
 (* generate the C code equivalent to [t1 bop t2]. *)
 and comparison_to_exp ?(loc=Location.unknown) ?e1 env bop t1 t2 t_opt =
   let ctx = match e1 with
-    | None -> principal_type_from_term t1 t2 
+    | None -> Typing.principal_type_from_term t1 t2 
     | Some(_, ctx) -> 
       (*      Options.feedback "principality oriented by %a" d_logic_type ctx;*)
-      principal_type_from_term { t1 with term_type = ctx } t2
+      Typing.principal_type_from_term { t1 with term_type = ctx } t2
   in
   (*  Options.feedback "principal type of %a and %a is %a" 
       d_term t1 d_term t2 d_logic_type ctx;*)
   let e1, env = match e1 with
     | None -> term_to_exp env ctx t1
     | Some(e1, ctx1) when Cil_datatype.Logic_type.equal ctx ctx1 -> e1, env
-    | Some(e1, _) -> context_sensitive ~loc:e1.eloc env ctx false (Some t1) e1
+    | Some(e1, _) -> 
+      Typing.context_sensitive ~loc:e1.eloc env ctx false (Some t1) e1
   in
   let e2, env = term_to_exp env ctx t2 in
   match ctx with
@@ -483,7 +338,7 @@ let rec named_predicate_to_exp env p =
     let e, env = 
       comparison_to_exp ~loc env (relation_to_binop rel) t1 t2 None 
     in
-    context_sensitive ~loc env (Ctype intType) false None e
+    Typing.context_sensitive ~loc env (Ctype intType) false None e
   | Pand(p1, p2) ->
     (* p1 && p2 <==> if p1 then p2 else false *)
     let e1, env1 = named_predicate_to_exp env p1 in
@@ -532,143 +387,7 @@ let rec named_predicate_to_exp env p =
   | Pif _ -> Error.not_yet "_ ? _ : _"
   | Plet _ -> Error.not_yet "let _ = _ in _"
   | Pforall(bounded_vars, { content = Pimplies(hyps, goal) }) -> 
-    (* universal quantification over integers (or a subtype of integer) *)
-    let guards = compute_quantif_guards p bounded_vars hyps in
-    let env = List.fold_left Env.Logic_binding.add env bounded_vars in
-    let var_res = ref Varinfo.dummy in
-    let res, env =
-      (* variable storing the result of the \forall *)
-      Env.new_var env None intType
-	(fun v _ ->
-	  var_res := v;
-	  let lv = var v in
-	  [ mkStmtOneInstr ~valid_sid:true (Set(lv, one ~loc, loc)) ])
-    in
-    let end_loop_ref = ref dummyStmt in
-    let rec mk_for_loop env = function
-      | [] -> 
-	(* innermost loop body: store the result in [res] and go out according
-	   to evaluation of the goal *)
-	let test, env = named_predicate_to_exp (Env.push env) goal in
- 	let then_block = mkBlock [ mkEmptyStmt ~loc () ] in
-	let else_block = 
-	  (* use a 'goto', not a simple 'break' in order to handle 'forall' with
-	     multiple binders (leading to imbricated loops) *)
-	  mkBlock
-	    [ mkStmtOneInstr
-		~valid_sid:true (Set(var !var_res, zero ~loc, loc));
-	      mkStmt ~valid_sid:true (Goto(end_loop_ref, loc)) ]
-	in
-	let blk, env = 
-	  Env.pop_and_get
-	    env
-	    (mkStmt ~valid_sid:true (If(test, then_block, else_block, loc)))
-	    ~global_clear:false
-	    Env.After
-	in
-	(* TODO: could be optimised if [pop_and_get] would return a list of
-	   stmts *)
-	[ mkStmt ~valid_sid:true (Block blk) ], env
-      | (t1, rel1, logic_x, rel2, t2) :: tl ->
-	let body, env = mk_for_loop env tl in
-	let t_plus_one t =
-	  Logic_const.term ~loc
-	    (TBinOp(PlusA, t, Logic_const.tinteger ~loc ~ikind:IChar 1))
-	    Linteger
-	in
-	let t1 = match rel1 with
-	  | Rlt -> t_plus_one t1
-	  | Rle -> t1
-	  | Rgt | Rge | Req | Rneq -> assert false
-	in
-	let bop2 = match rel2 with
-	  | Rlt -> Lt
-	  | Rle -> Le
-	  | Rgt | Rge | Req | Rneq -> assert false
-	in
-	(* we increment the loop counter one more time (at the end of the
-	   loop). Thus to prevent  overflow, check the type of [t2 + 1] instead
-	   of [t2]. *) 
-	let ty = principal_type_from_term t1 (t_plus_one t2) in
-	let ty = principal_type ty logic_x.lv_type in
-	(* loop counter corresponding to the quantified variable *)
-	let var_x = Env.Logic_binding.get env logic_x in
-	let lv_x = var var_x in
-	let x = new_exp ~loc (Lval lv_x) in
-	let env = match ty with
-	  | Ctype ty when isIntegralType ty -> 
-	    var_x.vtype <- ty;
-	    env
-	  | Linteger -> 
-	    var_x.vtype <- Mpz.t;
-	    Env.add_stmt env (Mpz.init x)
-	  | Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ -> assert false
-	in
-	(* initialize the loop counter to [t1] *)
-	let e1, env = term_to_exp (Env.push env) ty t1 in
-	let init_blk, env = 
-	  Env.pop_and_get 
-	    env
-	    (Mpz.affect lv_x x e1)
-	    ~global_clear:false
-	    Env.Middle
-	in
-	(* generate the guard [x bop t2] *)
-	let stmts_block b = [ mkStmt ~valid_sid:true (Block b) ] in
-	let tlv = Logic_const.tvar ~loc (cvar_to_lvar var_x) in
-	let guard_exp, env = 
-	  term_to_exp
-	    (Env.push env)
-	    (Ctype intType)
-	    (Logic_const.term (TBinOp(bop2, tlv, t2)) ty)
-	in
-	let break_stmt = mkStmt ~valid_sid:true (Break guard_exp.eloc) in
-	let guard_blk, env =
-	  Env.pop_and_get
-	    env
-	    (mkStmt ~valid_sid:true
-	       (If(guard_exp,
-		   mkBlock [ mkEmptyStmt () ],
-		   mkBlock [ break_stmt ], 
-		   guard_exp.eloc)))
-	    ~global_clear:false
-	    Env.Middle
-	in
-	let guard = stmts_block guard_blk in
-	(* increment the loop counter [x++] *)
-	let incr, env = term_to_exp (Env.push env) ty (t_plus_one tlv) in
-	let next_blk, env = 
-	  Env.pop_and_get
-	    env
-	    (Mpz.affect lv_x x incr)
-	    ~global_clear:false
-	    Env.Middle
-	in
-	(* generate the whole loop *)
-	let start = stmts_block init_blk in
-	let next = stmts_block next_blk in
-	start @
-	  [ mkStmt ~valid_sid:true
-	      (Loop ([],
-		     mkBlock (guard @ body @ next),
-		     loc, 
-		     None, 
-		     Some break_stmt)) ], 
-	env
-    in
-    let stmts, env = mk_for_loop env guards in
-    let env = 
-      Env.add_stmt env (mkStmt ~valid_sid:true (Block (mkBlock stmts))) 
-    in
-    (* where to jump to go out of the loop *)
-    let end_loop = mkEmptyStmt ~loc () in
-    let label_name = "e_acsl_end_loop" ^ string_of_int (Label_ids.next ()) in
-    let label = Label(label_name, loc, false) in
-    end_loop.labels <- label :: end_loop.labels;
-    end_loop_ref := end_loop;
-    let env = Env.add_stmt env end_loop in
-    let env = List.fold_left Env.Logic_binding.remove env bounded_vars in
-    res, env
+    Quantif.convert env loc p bounded_vars hyps goal
   | Pforall _ -> Error.not_yet "unguarded \\forall quantification"
   (*  | Pexists(bounded_vars, { content = Pand(hyps, _goal) }) -> 
       let guards = compute_quantif_guards p bounded_vars hyps in
@@ -688,6 +407,10 @@ let rec named_predicate_to_exp env p =
   | Psubtype _ -> Error.not_yet "subtyping relation" (* Jessie specific *)
   | Pinitialized _ -> Error.not_yet "\\initialized"
 
+let () = 
+  Quantif.term_to_exp_ref := term_to_exp;
+  Quantif.named_predicate_to_exp_ref := named_predicate_to_exp
+
 (* ************************************************************************** *)
 (* [convert_*] converts a given ACSL annotation into the corresponding C
    statement (if any) for runtime assertion checking *)