From 7a91deafcf4b7903bed8f1d4334e5abe4e286816 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 19 May 2016 20:09:47 +0200
Subject: [PATCH] [typing] mutable environment in inference system [typing] fix
bug in on-the-fly typing when translating quantification [typing] update a
few oracles
---
src/plugins/e-acsl/interval.ml | 58 ++--
src/plugins/e-acsl/interval.mli | 7 +-
src/plugins/e-acsl/quantif.ml | 44 +--
.../e-acsl-runtime/oracle/gen_linear_search.c | 6 +-
.../e-acsl-runtime/oracle/gen_mainargs.c | 54 ++--
.../e-acsl-runtime/oracle/mainargs.res.oracle | 9 +-
.../e-acsl/tests/gmp/oracle/gen_quantif2.c | 156 +++++-----
.../tests/gmp/oracle/quantif.1.res.oracle | 3 +-
src/plugins/e-acsl/translate.ml | 7 +-
src/plugins/e-acsl/typing.ml | 283 +++++++++---------
src/plugins/e-acsl/typing.mli | 8 +-
11 files changed, 329 insertions(+), 306 deletions(-)
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 225eae850ca..edadf8f7b5b 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -85,10 +85,10 @@ let join i1 i2 =
module Env = struct
open Cil_datatype
- type t = interv Logic_var.Map.t
- let empty = Logic_var.Map.empty
- let add = Logic_var.Map.add
- let find = Logic_var.Map.find
+ let tbl: interv Logic_var.Hashtbl.t = Logic_var.Hashtbl.create 7
+ let clear () = Logic_var.Hashtbl.clear tbl
+ let add = Logic_var.Hashtbl.add tbl
+ let find = Logic_var.Hashtbl.find tbl
end
(* ********************************************************************* *)
@@ -112,7 +112,7 @@ let infer_sizeof ty =
let infer_alignof ty = singleton_of_int (Cil.bytesAlignOf ty)
-let rec infer env t =
+let rec infer t =
let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in
match t.term_node with
| TConst (Integer (n,_)) -> make n n
@@ -126,7 +126,7 @@ let rec infer env t =
in
let n = Integer.of_int (find_idx 0 enumitem.eihost.eitems) in
make n n
- | TLval lv -> infer_term_lval env lv
+ | TLval lv -> infer_term_lval lv
| TSizeOf ty -> infer_sizeof ty
| TSizeOfE t -> infer_sizeof (get_cty t)
| TSizeOfStr str -> singleton_of_int (String.length str + 1 (* '\0' *))
@@ -134,10 +134,10 @@ let rec infer env t =
| TAlignOfE t -> infer_alignof (get_cty t)
| TUnOp (Neg, t) ->
- let { lower; upper } = infer env t in
+ let { lower; upper } = infer t in
make (Integer.neg upper) (Integer.neg lower)
| TUnOp (BNot, t) ->
- let { lower; upper } = infer env t in
+ let { lower; upper } = infer t in
let nl = Integer.lognot lower in
let nu = Integer.lognot upper in
make (Integer.min nl nu) (Integer.max nl nu)
@@ -146,20 +146,20 @@ let rec infer env t =
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _) ->
make Integer.zero Integer.one
| TBinOp (PlusA, t1, t2) ->
- let i1 = infer env t1 in
- let i2 = infer env t2 in
+ let i1 = infer t1 in
+ let i2 = infer t2 in
make (Integer.add i1.lower i2.lower) (Integer.add i1.upper i2.upper)
| TBinOp (MinusA, t1, t2) ->
- let i1 = infer env t1 in
- let i2 = infer env t2 in
+ let i1 = infer t1 in
+ let i2 = infer t2 in
make (Integer.sub i1.lower i2.upper) (Integer.sub i1.upper i2.lower)
| TBinOp (Mult, t1, t2) ->
- let i1 = infer env t1 in
- let i2 = infer env t2 in
+ let i1 = infer t1 in
+ let i2 = infer t2 in
combine Integer.mul i1 i2
| TBinOp (Div, t1, t2) ->
- let i1 = infer env t1 in
- let i2 = infer env t2 in
+ let i1 = infer t1 in
+ let i2 = infer t2 in
if Integer.le i2.lower Integer.zero && Integer.ge i2.upper Integer.zero then
(* 0 \in i2 *)
let l = Integer.min i1.lower (Integer.neg i1.upper) in
@@ -172,8 +172,8 @@ let rec infer env t =
in
combine div i1 i2
| TBinOp (Mod, t1, t2) ->
- let i1 = infer env t1 in
- let i2 = infer env t2 in
+ let i1 = infer t1 in
+ let i2 = infer t2 in
(* the sign of the result is the sign of [t1];
also no more elements than [t2-1] and no more than [t1] *)
let nb1 = Integer.max (Integer.abs i1.lower) (Integer.abs i1.upper) in
@@ -198,14 +198,14 @@ let rec infer env t =
| TCastE (ty, t)
| TCoerce (t, ty) ->
- let it = infer env t in
+ let it = infer t in
let ity = interv_of_typ ty in
meet it ity
| Tif (_, t2, t3) ->
- let i2 = infer env t2 in
- let i3 = infer env t3 in
+ let i2 = infer t2 in
+ let i3 = infer t3 in
join i2 i3
- | Tat (t, _) -> infer env t
+ | Tat (t, _) -> infer t
| TBinOp (MinusPP, t, _) ->
(match Cil.unrollType (get_cty t) with
| TArray(_, _, { scache = Computed n }, _) ->
@@ -221,10 +221,10 @@ let rec infer env t =
| TArray _ | TPtr _ -> Lazy.force interv_of_unknown_block
| _ -> assert false)
| Tnull -> singleton_of_int 0
- | TLogic_coerce (_, t) -> infer env t
+ | TLogic_coerce (_, t) -> infer t
| TCoerceE (t1, t2) ->
- let i1 = infer env t1 in
- let i2 = infer env t2 in
+ let i1 = infer t1 in
+ let i2 = infer t2 in
meet i1 i2
| Tapp (_,_,_) -> Error.not_yet "logic function application"
@@ -248,16 +248,16 @@ let rec infer env t =
| Ttype _
| Tempty_set -> raise Not_an_integer
-and infer_term_lval env (host, offset as tlv) =
+and infer_term_lval (host, offset as tlv) =
match offset with
- | TNoOffset -> infer_term_host env host
+ | TNoOffset -> infer_term_host host
| _ ->
let ty = Logic_utils.logicCType (Cil.typeOfTermLval tlv) in
interv_of_typ ty
-and infer_term_host env = function
+and infer_term_host = function
| TVar v ->
- (try Env.find v env
+ (try Env.find v
with Not_found -> interv_of_typ (Logic_utils.logicCType v.lv_type))
| TResult ty -> interv_of_typ ty
| TMem t ->
diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli
index f6a906c3c2b..456310f5833 100644
--- a/src/plugins/e-acsl/interval.mli
+++ b/src/plugins/e-acsl/interval.mli
@@ -29,9 +29,8 @@ type interv = private { lower: Integer.t; upper: Integer.t }
include Datatype.S with type t = interv
module Env: sig
- type t
- val empty: t
- val add: Cil_types.logic_var -> interv -> t -> t
+ val clear: unit -> unit
+ val add: Cil_types.logic_var -> interv -> unit
end
val interv_of_typ: Cil_types.typ -> t
@@ -41,7 +40,7 @@ val join: t -> t -> t
val meet: t -> t -> t
exception Not_an_integer
-val infer: Env.t -> Cil_types.term -> t
+val infer: Cil_types.term -> t
(** [infer t] infers the smallest possible integer interval which the values
of the term can fit in. Assume than the type of [t] is an integral type.
@raise Not_an_integer if the type of the term is not a subtype of
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index b6daa15f265..e4a9e47fbf3 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -168,7 +168,6 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
let ty2 = Typing.get_integer_ty t2 in
Typing.join ty1 ty2
in
- let ty = Typing.typ_of_integer_ty ctx in
let t_plus_one t =
Logic_const.term ~loc
(TBinOp(PlusA, t, Logic_const.tinteger ~loc 1))
@@ -177,7 +176,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
let t1 = match rel1 with
| Rlt ->
let t = t_plus_one t1 in
- Typing.type_term ~ctx t;
+ Typing.type_term ~force:true ~ctx t;
t
| Rle -> t1
| Rgt | Rge | Req | Rneq -> assert false
@@ -186,35 +185,46 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
| Rlt -> t2, Lt
| Rle ->
(* we increment the loop counter one more time (at the end of the
- loop). Thus to prevent overflow, check the type of [t2 + 1]
+ loop). Thus to prevent overflow, check the type of [t2+1]
instead of [t2]. *)
t_plus_one t2, Le
| Rgt | Rge | Req | Rneq -> assert false
in
- Typing.type_term ~ctx t2_one;
+ Typing.type_term ~force:true ~ctx t2_one;
+ let ctx_one =
+ let ty1 = Typing.get_integer_ty t1 in
+ let ty2 = Typing.get_integer_ty t2_one in
+ Typing.join ty1 ty2
+ in
+ let ty = Typing.typ_of_integer_ty ctx_one in
(* loop counter corresponding to the quantified variable *)
let var_x, x, env = Env.Logic_binding.add ~ty env logic_x in
let lv_x = var var_x in
- let env =
- if Gmpz.is_t ty then Env.add_stmt env (Gmpz.init ~loc x) else env
+ let env = match ctx_one with
+ | Typing.C_type _ -> env
+ | Typing.Gmp -> Env.add_stmt env (Gmpz.init ~loc x)
+ | Typing.Other -> assert false
in
- let llv = cvar_to_lvar var_x in
(* build the inner loops and loop body *)
let body, env = mk_for_loop env tl in
(* initialize the loop counter to [t1] *)
let e1, env = term_to_exp kf (Env.push env) t1 in
- let init_blk, env =
- Env.pop_and_get
- env
- (Gmpz.affect ~loc:e1.eloc lv_x x e1)
- ~global_clear:false
- Env.Middle
+ let init_blk, env =
+ Env.pop_and_get
+ env
+ (Gmpz.affect ~loc:e1.eloc 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 llv in
- let guard = Logic_const.term ~loc (TBinOp(bop2, tlv, t2)) Linteger in
- Typing.type_term ~ctx:Typing.c_int guard;
+ let tlv = Logic_const.tvar ~loc logic_x in
+ let guard =
+ (* must copy [t2] to force being typed again *)
+ Logic_const.term ~loc
+ (TBinOp(bop2, tlv, { t2 with term_node = t2.term_node } )) Linteger
+ in
+ Typing.type_term ~force:true ~ctx:Typing.c_int guard;
let guard_exp, env = term_to_exp kf (Env.push env) guard in
let break_stmt = mkStmt ~valid_sid:true (Break guard_exp.eloc) in
let guard_blk, env =
@@ -232,7 +242,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
(* increment the loop counter [x++] *)
let tlv_one = t_plus_one tlv in
(* previous typing ensures that [x++] fits type [ty] *)
- Typing.type_term ~ctx tlv_one;
+ Typing.type_term ~force:true ~ctx:ctx_one tlv_one;
let incr, env = term_to_exp kf (Env.push env) tlv_one in
let next_blk, env =
Env.pop_and_get
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
index 95fee64be9e..22b41d67d4e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
@@ -161,7 +161,7 @@ int __gen_e_acsl_search(int elt)
__gen_e_acsl_forall = 0;
goto e_acsl_end_loop3;
}
- __gen_e_acsl_i = (int)(__gen_e_acsl_i + 1L);
+ __gen_e_acsl_i ++;
}
e_acsl_end_loop3: ;
__e_acsl_assert(__gen_e_acsl_forall,(char *)"Precondition",
@@ -184,7 +184,7 @@ int __gen_e_acsl_search(int elt)
__gen_e_acsl_forall_2 = 0;
goto e_acsl_end_loop5;
}
- __gen_e_acsl_j_2 = (int)(__gen_e_acsl_j_2 + 1L);
+ __gen_e_acsl_j_2 ++;
}
e_acsl_end_loop5: ;
__gen_e_acsl_at_2 = __gen_e_acsl_forall_2;
@@ -205,7 +205,7 @@ int __gen_e_acsl_search(int elt)
__gen_e_acsl_exists = 1;
goto e_acsl_end_loop4;
}
- __gen_e_acsl_j = (int)(__gen_e_acsl_j + 1L);
+ __gen_e_acsl_j ++;
}
e_acsl_end_loop4: ;
__gen_e_acsl_at = __gen_e_acsl_exists;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
index c0192f76823..fb58b0114e3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
@@ -30,7 +30,7 @@ int main(int argc, char **argv)
if (__gen_e_acsl_k < argc) ; else break;
{
int __gen_e_acsl_valid_3;
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)(argv + __gen_e_acsl_k),
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)(argv + (unsigned long)__gen_e_acsl_k),
sizeof(char *));
if (__gen_e_acsl_valid_3) ;
else {
@@ -38,7 +38,7 @@ int main(int argc, char **argv)
goto e_acsl_end_loop1;
}
}
- __gen_e_acsl_k ++;
+ __gen_e_acsl_k = (int)(__gen_e_acsl_k + 1L);
}
e_acsl_end_loop1: ;
__e_acsl_assert(__gen_e_acsl_forall,(char *)"Assertion",(char *)"main",
@@ -53,7 +53,7 @@ int main(int argc, char **argv)
int __gen_e_acsl_eq;
__gen_e_acsl_block_length = __e_acsl_block_length((void *)argv);
__gmpz_init_set_ui(__gen_e_acsl_block_length_2,__gen_e_acsl_block_length);
- __gmpz_init_set_si(__gen_e_acsl_,((long)argc + (long)1) * 8L);
+ __gmpz_init_set_si(__gen_e_acsl_,(argc + 1) * 8);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_block_length_2),
(__mpz_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
@@ -65,29 +65,32 @@ int main(int argc, char **argv)
/*@ assert *(argv+argc) ≡ \null; */
{
int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(argv + argc),
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(argv + (unsigned long)argc),
sizeof(char *));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(argv+argc)",15);
- /*@ assert Value: mem_access: \valid_read(argv+argc); */
- __e_acsl_assert(*(argv + argc) == (void *)0,(char *)"Assertion",
- (char *)"main",(char *)"*(argv+argc) == \\null",15);
+ (char *)"mem_access: \\valid_read(argv+(unsigned long)argc)",
+ 15);
+ /*@ assert Value: mem_access: \valid_read(argv+(unsigned long)argc); */
+ __e_acsl_assert(*(argv + (unsigned long)argc) == (void *)0,
+ (char *)"Assertion",(char *)"main",
+ (char *)"*(argv+argc) == \\null",15);
}
/*@ assert ¬\valid(*(argv+argc)); */
{
int __gen_e_acsl_initialized;
int __gen_e_acsl_and;
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)(argv + argc),
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(argv + (unsigned long)argc),
sizeof(char *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_read_2;
int __gen_e_acsl_valid_4;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(argv + argc),
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(argv + (unsigned long)argc),
sizeof(char *));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(argv+argc)",16);
- /*@ assert Value: mem_access: \valid_read(argv+argc); */
- __gen_e_acsl_valid_4 = __e_acsl_valid((void *)*(argv + argc),
+ (char *)"mem_access: \\valid_read(argv+(unsigned long)argc)",
+ 16);
+ /*@ assert Value: mem_access: \valid_read(argv+(unsigned long)argc); */
+ __gen_e_acsl_valid_4 = __e_acsl_valid((void *)*(argv + (unsigned long)argc),
sizeof(char));
__gen_e_acsl_and = __gen_e_acsl_valid_4;
}
@@ -100,23 +103,27 @@ int main(int argc, char **argv)
{
int len;
size_t tmp;
+ /*@ assert Value: mem_access: \valid_read(argv+i); */
tmp = __gen_e_acsl_strlen((char const *)*(argv + i));
len = (int)tmp;
/*@ assert \valid(*(argv+i)); */
{
int __gen_e_acsl_initialized_2;
int __gen_e_acsl_and_2;
- __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(argv + i),
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(argv + (unsigned long)i),
sizeof(char *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_read_3;
int __gen_e_acsl_valid_5;
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(argv + i),
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(argv + (unsigned long)i),
sizeof(char *));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
(char *)"main",
- (char *)"mem_access: \\valid_read(argv+i)",19);
- __gen_e_acsl_valid_5 = __e_acsl_valid((void *)*(argv + i),
+ (char *)"mem_access: \\valid_read(argv+(unsigned long)i)",
+ 19);
+ /*@ assert Value: mem_access: \valid_read(argv+(unsigned long)i);
+ */
+ __gen_e_acsl_valid_5 = __e_acsl_valid((void *)*(argv + (unsigned long)i),
sizeof(char));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_5;
}
@@ -129,19 +136,22 @@ int main(int argc, char **argv)
int __gen_e_acsl_forall_2;
long __gen_e_acsl_k_2;
__gen_e_acsl_forall_2 = 1;
- __gen_e_acsl_k_2 = (long)0;
+ __gen_e_acsl_k_2 = 0;
while (1) {
- if (__gen_e_acsl_k_2 <= (long)len) ; else break;
+ if (__gen_e_acsl_k_2 <= len) ; else break;
{
int __gen_e_acsl_valid_read_4;
int __gen_e_acsl_valid_6;
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(
- argv + i),
+ argv + (unsigned long)i),
sizeof(char *));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",
(char *)"main",
- (char *)"mem_access: \\valid_read(argv+i)",20);
- __gen_e_acsl_valid_6 = __e_acsl_valid((void *)(*(argv + i) + __gen_e_acsl_k_2),
+ (char *)"mem_access: \\valid_read(argv+(unsigned long)i)",
+ 20);
+ /*@ assert Value: mem_access: \valid_read(argv+(unsigned long)i);
+ */
+ __gen_e_acsl_valid_6 = __e_acsl_valid((void *)(*(argv + (unsigned long)i) + (unsigned long)__gen_e_acsl_k_2),
sizeof(char));
if (__gen_e_acsl_valid_6) ;
else {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
index b07a36e3922..c6326144037 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle
@@ -6,18 +6,21 @@ FRAMAC_SHARE/libc/string.h:91:[e-acsl] warning: E-ACSL construct `logic function
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:91:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:93:[e-acsl] warning: E-ACSL construct `applying logic function' is not yet supported.
+FRAMAC_SHARE/libc/string.h:93:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/mainargs.c:12:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:13:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:15:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/mainargs.c:15:[value] warning: out of bounds read. assert \valid_read(argv+argc);
+tests/e-acsl-runtime/mainargs.c:15:[kernel] warning: out of bounds read. assert \valid_read(argv+(unsigned long)argc);
tests/e-acsl-runtime/mainargs.c:16:[value] warning: assertion got status unknown.
-tests/e-acsl-runtime/mainargs.c:16:[value] warning: out of bounds read. assert \valid_read(argv+argc);
+tests/e-acsl-runtime/mainargs.c:16:[kernel] warning: out of bounds read. assert \valid_read(argv+(unsigned long)argc);
FRAMAC_SHARE/libc/string.h:91:[value] warning: function __gen_e_acsl_strlen: precondition 'valid_string_src' got status unknown.
FRAMAC_SHARE/libc/string.h:91:[value] warning: function strlen: precondition 'valid_string_src' got status unknown.
FRAMAC_SHARE/libc/string.h:93:[value] warning: function __gen_e_acsl_strlen: postcondition got status unknown.
tests/e-acsl-runtime/mainargs.c:19:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:20:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/mainargs.c:18:[kernel] warning: out of bounds read. assert \valid_read(argv+i);
+tests/e-acsl-runtime/mainargs.c:19:[kernel] warning: out of bounds read. assert \valid_read(argv+(unsigned long)i);
+tests/e-acsl-runtime/mainargs.c:20:[kernel] warning: out of bounds read. assert \valid_read(argv+(unsigned long)i);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
index 14ccacd711a..cb4a5be8286 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
@@ -10,7 +10,7 @@ int main(void)
__gmpz_init(__gen_e_acsl_x);
{
mpz_t __gen_e_acsl__3;
- __gmpz_init_set_si(__gen_e_acsl__3,(long)0);
+ __gmpz_init_set_ui(__gen_e_acsl__3,(unsigned long)0);
__gmpz_set(__gen_e_acsl_x,(__mpz_struct const *)(__gen_e_acsl__3));
__gmpz_clear(__gen_e_acsl__3);
}
@@ -18,7 +18,7 @@ int main(void)
{
mpz_t __gen_e_acsl__4;
int __gen_e_acsl_le;
- __gmpz_init_set_si(__gen_e_acsl__4,(long)1);
+ __gmpz_init_set_ui(__gen_e_acsl__4,(unsigned long)1);
__gen_e_acsl_le = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x),
(__mpz_struct const *)(__gen_e_acsl__4));
if (__gen_e_acsl_le <= 0) ; else break;
@@ -28,14 +28,14 @@ int main(void)
mpz_t __gen_e_acsl_;
int __gen_e_acsl_eq;
int __gen_e_acsl_or;
- __gmpz_init_set_si(__gen_e_acsl_,(long)0);
+ __gmpz_init_set_ui(__gen_e_acsl_,(unsigned long)0);
__gen_e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x),
(__mpz_struct const *)(__gen_e_acsl_));
if (__gen_e_acsl_eq == 0) __gen_e_acsl_or = 1;
else {
mpz_t __gen_e_acsl__2;
int __gen_e_acsl_eq_2;
- __gmpz_init_set_si(__gen_e_acsl__2,(long)1);
+ __gmpz_init_set_ui(__gen_e_acsl__2,(unsigned long)1);
__gen_e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x),
(__mpz_struct const *)(__gen_e_acsl__2));
__gen_e_acsl_or = __gen_e_acsl_eq_2 == 0;
@@ -51,7 +51,7 @@ int main(void)
{
mpz_t __gen_e_acsl__5;
mpz_t __gen_e_acsl_add;
- __gmpz_init_set_si(__gen_e_acsl__5,1L);
+ __gmpz_init_set_ui(__gen_e_acsl__5,1UL);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)(__gen_e_acsl_x),
(__mpz_struct const *)(__gen_e_acsl__5));
@@ -76,8 +76,8 @@ int main(void)
mpz_t __gen_e_acsl__7;
mpz_t __gen_e_acsl__8;
mpz_t __gen_e_acsl_add_2;
- __gmpz_init_set_si(__gen_e_acsl__7,(long)0);
- __gmpz_init_set_si(__gen_e_acsl__8,1L);
+ __gmpz_init_set_ui(__gen_e_acsl__7,(unsigned long)0);
+ __gmpz_init_set_ui(__gen_e_acsl__8,1UL);
__gmpz_init(__gen_e_acsl_add_2);
__gmpz_add(__gen_e_acsl_add_2,(__mpz_struct const *)(__gen_e_acsl__7),
(__mpz_struct const *)(__gen_e_acsl__8));
@@ -90,7 +90,7 @@ int main(void)
{
mpz_t __gen_e_acsl__9;
int __gen_e_acsl_le_2;
- __gmpz_init_set_si(__gen_e_acsl__9,(long)1);
+ __gmpz_init_set_ui(__gen_e_acsl__9,(unsigned long)1);
__gen_e_acsl_le_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_2),
(__mpz_struct const *)(__gen_e_acsl__9));
if (__gen_e_acsl_le_2 <= 0) ; else break;
@@ -99,7 +99,7 @@ int main(void)
{
mpz_t __gen_e_acsl__6;
int __gen_e_acsl_eq_3;
- __gmpz_init_set_si(__gen_e_acsl__6,(long)1);
+ __gmpz_init_set_ui(__gen_e_acsl__6,(unsigned long)1);
__gen_e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_2),
(__mpz_struct const *)(__gen_e_acsl__6));
__gmpz_clear(__gen_e_acsl__6);
@@ -112,7 +112,7 @@ int main(void)
{
mpz_t __gen_e_acsl__10;
mpz_t __gen_e_acsl_add_3;
- __gmpz_init_set_si(__gen_e_acsl__10,1L);
+ __gmpz_init_set_ui(__gen_e_acsl__10,1UL);
__gmpz_init(__gen_e_acsl_add_3);
__gmpz_add(__gen_e_acsl_add_3,
(__mpz_struct const *)(__gen_e_acsl_x_2),
@@ -138,8 +138,8 @@ int main(void)
mpz_t __gen_e_acsl__11;
mpz_t __gen_e_acsl__12;
mpz_t __gen_e_acsl_add_4;
- __gmpz_init_set_si(__gen_e_acsl__11,(long)0);
- __gmpz_init_set_si(__gen_e_acsl__12,1L);
+ __gmpz_init_set_ui(__gen_e_acsl__11,(unsigned long)0);
+ __gmpz_init_set_ui(__gen_e_acsl__12,1UL);
__gmpz_init(__gen_e_acsl_add_4);
__gmpz_add(__gen_e_acsl_add_4,(__mpz_struct const *)(__gen_e_acsl__11),
(__mpz_struct const *)(__gen_e_acsl__12));
@@ -152,7 +152,7 @@ int main(void)
{
mpz_t __gen_e_acsl__13;
int __gen_e_acsl_lt;
- __gmpz_init_set_si(__gen_e_acsl__13,(long)1);
+ __gmpz_init_set_ui(__gen_e_acsl__13,(unsigned long)1);
__gen_e_acsl_lt = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_3),
(__mpz_struct const *)(__gen_e_acsl__13));
if (__gen_e_acsl_lt < 0) ; else break;
@@ -166,7 +166,7 @@ int main(void)
{
mpz_t __gen_e_acsl__14;
mpz_t __gen_e_acsl_add_5;
- __gmpz_init_set_si(__gen_e_acsl__14,1L);
+ __gmpz_init_set_ui(__gen_e_acsl__14,1UL);
__gmpz_init(__gen_e_acsl_add_5);
__gmpz_add(__gen_e_acsl_add_5,
(__mpz_struct const *)(__gen_e_acsl_x_3),
@@ -190,7 +190,7 @@ int main(void)
__gmpz_init(__gen_e_acsl_x_4);
{
mpz_t __gen_e_acsl__16;
- __gmpz_init_set_si(__gen_e_acsl__16,(long)0);
+ __gmpz_init_set_ui(__gen_e_acsl__16,(unsigned long)0);
__gmpz_set(__gen_e_acsl_x_4,(__mpz_struct const *)(__gen_e_acsl__16));
__gmpz_clear(__gen_e_acsl__16);
}
@@ -198,7 +198,7 @@ int main(void)
{
mpz_t __gen_e_acsl__17;
int __gen_e_acsl_lt_2;
- __gmpz_init_set_si(__gen_e_acsl__17,(long)1);
+ __gmpz_init_set_ui(__gen_e_acsl__17,(unsigned long)1);
__gen_e_acsl_lt_2 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_4),
(__mpz_struct const *)(__gen_e_acsl__17));
if (__gen_e_acsl_lt_2 < 0) ; else break;
@@ -207,7 +207,7 @@ int main(void)
{
mpz_t __gen_e_acsl__15;
int __gen_e_acsl_eq_4;
- __gmpz_init_set_si(__gen_e_acsl__15,(long)0);
+ __gmpz_init_set_ui(__gen_e_acsl__15,(unsigned long)0);
__gen_e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_4),
(__mpz_struct const *)(__gen_e_acsl__15));
__gmpz_clear(__gen_e_acsl__15);
@@ -220,7 +220,7 @@ int main(void)
{
mpz_t __gen_e_acsl__18;
mpz_t __gen_e_acsl_add_6;
- __gmpz_init_set_si(__gen_e_acsl__18,1L);
+ __gmpz_init_set_ui(__gen_e_acsl__18,1UL);
__gmpz_init(__gen_e_acsl_add_6);
__gmpz_add(__gen_e_acsl_add_6,
(__mpz_struct const *)(__gen_e_acsl_x_4),
@@ -251,7 +251,7 @@ int main(void)
__gmpz_init(__gen_e_acsl_z);
{
mpz_t __gen_e_acsl__25;
- __gmpz_init_set_si(__gen_e_acsl__25,(long)0);
+ __gmpz_init_set_ui(__gen_e_acsl__25,(unsigned long)0);
__gmpz_set(__gen_e_acsl_x_5,(__mpz_struct const *)(__gen_e_acsl__25));
__gmpz_clear(__gen_e_acsl__25);
}
@@ -259,7 +259,7 @@ int main(void)
{
mpz_t __gen_e_acsl__26;
int __gen_e_acsl_lt_4;
- __gmpz_init_set_si(__gen_e_acsl__26,(long)2);
+ __gmpz_init_set_ui(__gen_e_acsl__26,(unsigned long)2);
__gen_e_acsl_lt_4 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_5),
(__mpz_struct const *)(__gen_e_acsl__26));
if (__gen_e_acsl_lt_4 < 0) ; else break;
@@ -267,7 +267,7 @@ int main(void)
}
{
mpz_t __gen_e_acsl__22;
- __gmpz_init_set_si(__gen_e_acsl__22,(long)0);
+ __gmpz_init_set_ui(__gen_e_acsl__22,(unsigned long)0);
__gmpz_set(__gen_e_acsl_y,(__mpz_struct const *)(__gen_e_acsl__22));
__gmpz_clear(__gen_e_acsl__22);
}
@@ -275,7 +275,7 @@ int main(void)
{
mpz_t __gen_e_acsl__23;
int __gen_e_acsl_lt_3;
- __gmpz_init_set_si(__gen_e_acsl__23,(long)5);
+ __gmpz_init_set_ui(__gen_e_acsl__23,(unsigned long)5);
__gen_e_acsl_lt_3 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_y),
(__mpz_struct const *)(__gen_e_acsl__23));
if (__gen_e_acsl_lt_3 < 0) ; else break;
@@ -283,7 +283,7 @@ int main(void)
}
{
mpz_t __gen_e_acsl__20;
- __gmpz_init_set_si(__gen_e_acsl__20,(long)0);
+ __gmpz_init_set_ui(__gen_e_acsl__20,(unsigned long)0);
__gmpz_set(__gen_e_acsl_z,(__mpz_struct const *)(__gen_e_acsl__20));
__gmpz_clear(__gen_e_acsl__20);
}
@@ -303,7 +303,7 @@ int main(void)
__gmpz_add(__gen_e_acsl_add_7,
(__mpz_struct const *)(__gen_e_acsl_x_5),
(__mpz_struct const *)(__gen_e_acsl_z));
- __gmpz_init_set_si(__gen_e_acsl__19,(long)1);
+ __gmpz_init_set_ui(__gen_e_acsl__19,(unsigned long)1);
__gmpz_init(__gen_e_acsl_add_8);
__gmpz_add(__gen_e_acsl_add_8,
(__mpz_struct const *)(__gen_e_acsl_y),
@@ -322,7 +322,7 @@ int main(void)
{
mpz_t __gen_e_acsl__21;
mpz_t __gen_e_acsl_add_9;
- __gmpz_init_set_si(__gen_e_acsl__21,1L);
+ __gmpz_init_set_ui(__gen_e_acsl__21,1UL);
__gmpz_init(__gen_e_acsl_add_9);
__gmpz_add(__gen_e_acsl_add_9,
(__mpz_struct const *)(__gen_e_acsl_z),
@@ -336,7 +336,7 @@ int main(void)
{
mpz_t __gen_e_acsl__24;
mpz_t __gen_e_acsl_add_10;
- __gmpz_init_set_si(__gen_e_acsl__24,1L);
+ __gmpz_init_set_ui(__gen_e_acsl__24,1UL);
__gmpz_init(__gen_e_acsl_add_10);
__gmpz_add(__gen_e_acsl_add_10,
(__mpz_struct const *)(__gen_e_acsl_y),
@@ -350,7 +350,7 @@ int main(void)
{
mpz_t __gen_e_acsl__27;
mpz_t __gen_e_acsl_add_11;
- __gmpz_init_set_si(__gen_e_acsl__27,1L);
+ __gmpz_init_set_ui(__gen_e_acsl__27,1UL);
__gmpz_init(__gen_e_acsl_add_11);
__gmpz_add(__gen_e_acsl_add_11,
(__mpz_struct const *)(__gen_e_acsl_x_5),
@@ -375,26 +375,21 @@ int main(void)
mpz_t __gen_e_acsl_x_6;
__gen_e_acsl_exists = 0;
__gmpz_init(__gen_e_acsl_x_6);
- {
- mpz_t __gen_e_acsl__29;
- __gmpz_init_set_si(__gen_e_acsl__29,(long)0);
- __gmpz_set(__gen_e_acsl_x_6,(__mpz_struct const *)(__gen_e_acsl__29));
- __gmpz_clear(__gen_e_acsl__29);
- }
+ __gmpz_set_si(__gen_e_acsl_x_6,(long)0);
while (1) {
{
- mpz_t __gen_e_acsl__30;
+ mpz_t __gen_e_acsl__29;
int __gen_e_acsl_lt_5;
- __gmpz_init_set_si(__gen_e_acsl__30,(long)10);
+ __gmpz_init_set_ui(__gen_e_acsl__29,(unsigned long)10);
__gen_e_acsl_lt_5 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_6),
- (__mpz_struct const *)(__gen_e_acsl__30));
+ (__mpz_struct const *)(__gen_e_acsl__29));
if (__gen_e_acsl_lt_5 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__30);
+ __gmpz_clear(__gen_e_acsl__29);
}
{
mpz_t __gen_e_acsl__28;
int __gen_e_acsl_eq_5;
- __gmpz_init_set_si(__gen_e_acsl__28,(long)5);
+ __gmpz_init_set_ui(__gen_e_acsl__28,(unsigned long)5);
__gen_e_acsl_eq_5 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_6),
(__mpz_struct const *)(__gen_e_acsl__28));
__gmpz_clear(__gen_e_acsl__28);
@@ -405,16 +400,16 @@ int main(void)
}
}
{
- mpz_t __gen_e_acsl__31;
+ mpz_t __gen_e_acsl__30;
mpz_t __gen_e_acsl_add_12;
- __gmpz_init_set_si(__gen_e_acsl__31,1L);
+ __gmpz_init_set_ui(__gen_e_acsl__30,1UL);
__gmpz_init(__gen_e_acsl_add_12);
__gmpz_add(__gen_e_acsl_add_12,
(__mpz_struct const *)(__gen_e_acsl_x_6),
- (__mpz_struct const *)(__gen_e_acsl__31));
+ (__mpz_struct const *)(__gen_e_acsl__30));
__gmpz_set(__gen_e_acsl_x_6,
(__mpz_struct const *)(__gen_e_acsl_add_12));
- __gmpz_clear(__gen_e_acsl__31);
+ __gmpz_clear(__gen_e_acsl__30);
__gmpz_clear(__gen_e_acsl_add_12);
}
}
@@ -433,42 +428,37 @@ int main(void)
mpz_t __gen_e_acsl_x_7;
__gen_e_acsl_forall_6 = 1;
__gmpz_init(__gen_e_acsl_x_7);
- {
- mpz_t __gen_e_acsl__39;
- __gmpz_init_set_si(__gen_e_acsl__39,(long)0);
- __gmpz_set(__gen_e_acsl_x_7,(__mpz_struct const *)(__gen_e_acsl__39));
- __gmpz_clear(__gen_e_acsl__39);
- }
+ __gmpz_set_si(__gen_e_acsl_x_7,(long)0);
while (1) {
{
- mpz_t __gen_e_acsl__40;
+ mpz_t __gen_e_acsl__38;
int __gen_e_acsl_lt_6;
- __gmpz_init_set_si(__gen_e_acsl__40,(long)10);
+ __gmpz_init_set_ui(__gen_e_acsl__38,(unsigned long)10);
__gen_e_acsl_lt_6 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_7),
- (__mpz_struct const *)(__gen_e_acsl__40));
+ (__mpz_struct const *)(__gen_e_acsl__38));
if (__gen_e_acsl_lt_6 < 0) ; else break;
- __gmpz_clear(__gen_e_acsl__40);
+ __gmpz_clear(__gen_e_acsl__38);
}
{
+ mpz_t __gen_e_acsl__31;
mpz_t __gen_e_acsl__32;
- mpz_t __gen_e_acsl__33;
int __gen_e_acsl_mod_guard;
mpz_t __gen_e_acsl_mod;
int __gen_e_acsl_eq_6;
int __gen_e_acsl_implies;
- __gmpz_init_set_si(__gen_e_acsl__32,(long)2);
- __gmpz_init_set_si(__gen_e_acsl__33,0L);
- __gen_e_acsl_mod_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__32),
- (__mpz_struct const *)(__gen_e_acsl__33));
+ __gmpz_init_set_ui(__gen_e_acsl__31,(unsigned long)2);
+ __gmpz_init_set_ui(__gen_e_acsl__32,0UL);
+ __gen_e_acsl_mod_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__31),
+ (__mpz_struct const *)(__gen_e_acsl__32));
__gmpz_init(__gen_e_acsl_mod);
/*@ assert E_ACSL: 2 ≢ 0; */
__e_acsl_assert(! (__gen_e_acsl_mod_guard == 0),(char *)"Assertion",
(char *)"main",(char *)"2 == 0",26);
__gmpz_tdiv_r(__gen_e_acsl_mod,
(__mpz_struct const *)(__gen_e_acsl_x_7),
- (__mpz_struct const *)(__gen_e_acsl__32));
+ (__mpz_struct const *)(__gen_e_acsl__31));
__gen_e_acsl_eq_6 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_mod),
- (__mpz_struct const *)(__gen_e_acsl__33));
+ (__mpz_struct const *)(__gen_e_acsl__32));
if (! (__gen_e_acsl_eq_6 == 0)) __gen_e_acsl_implies = 1;
else {
int __gen_e_acsl_exists_2;
@@ -476,23 +466,23 @@ int main(void)
__gen_e_acsl_exists_2 = 0;
__gmpz_init(__gen_e_acsl_y_2);
{
- mpz_t __gen_e_acsl__35;
- __gmpz_init_set_si(__gen_e_acsl__35,(long)0);
+ mpz_t __gen_e_acsl__34;
+ __gmpz_init_set_ui(__gen_e_acsl__34,(unsigned long)0);
__gmpz_set(__gen_e_acsl_y_2,
- (__mpz_struct const *)(__gen_e_acsl__35));
- __gmpz_clear(__gen_e_acsl__35);
+ (__mpz_struct const *)(__gen_e_acsl__34));
+ __gmpz_clear(__gen_e_acsl__34);
}
while (1) {
{
+ mpz_t __gen_e_acsl__35;
mpz_t __gen_e_acsl__36;
- mpz_t __gen_e_acsl__37;
int __gen_e_acsl_div_guard;
mpz_t __gen_e_acsl_div;
int __gen_e_acsl_le_5;
- __gmpz_init_set_si(__gen_e_acsl__36,(long)2);
- __gmpz_init_set_si(__gen_e_acsl__37,0L);
- __gen_e_acsl_div_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__36),
- (__mpz_struct const *)(__gen_e_acsl__37));
+ __gmpz_init_set_ui(__gen_e_acsl__35,(unsigned long)2);
+ __gmpz_init_set_ui(__gen_e_acsl__36,0UL);
+ __gen_e_acsl_div_guard = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl__35),
+ (__mpz_struct const *)(__gen_e_acsl__36));
__gmpz_init(__gen_e_acsl_div);
/*@ assert E_ACSL: 2 ≢ 0; */
__e_acsl_assert(! (__gen_e_acsl_div_guard == 0),
@@ -500,26 +490,26 @@ int main(void)
(char *)"2 == 0",26);
__gmpz_tdiv_q(__gen_e_acsl_div,
(__mpz_struct const *)(__gen_e_acsl_x_7),
- (__mpz_struct const *)(__gen_e_acsl__36));
+ (__mpz_struct const *)(__gen_e_acsl__35));
__gen_e_acsl_le_5 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_y_2),
(__mpz_struct const *)(__gen_e_acsl_div));
if (__gen_e_acsl_le_5 <= 0) ; else break;
+ __gmpz_clear(__gen_e_acsl__35);
__gmpz_clear(__gen_e_acsl__36);
- __gmpz_clear(__gen_e_acsl__37);
__gmpz_clear(__gen_e_acsl_div);
}
{
- mpz_t __gen_e_acsl__34;
+ mpz_t __gen_e_acsl__33;
mpz_t __gen_e_acsl_mul;
int __gen_e_acsl_eq_7;
- __gmpz_init_set_si(__gen_e_acsl__34,(long)2);
+ __gmpz_init_set_ui(__gen_e_acsl__33,(unsigned long)2);
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,
- (__mpz_struct const *)(__gen_e_acsl__34),
+ (__mpz_struct const *)(__gen_e_acsl__33),
(__mpz_struct const *)(__gen_e_acsl_y_2));
__gen_e_acsl_eq_7 = __gmpz_cmp((__mpz_struct const *)(__gen_e_acsl_x_7),
(__mpz_struct const *)(__gen_e_acsl_mul));
- __gmpz_clear(__gen_e_acsl__34);
+ __gmpz_clear(__gen_e_acsl__33);
__gmpz_clear(__gen_e_acsl_mul);
if (! (__gen_e_acsl_eq_7 == 0)) ;
else {
@@ -528,16 +518,16 @@ int main(void)
}
}
{
- mpz_t __gen_e_acsl__38;
+ mpz_t __gen_e_acsl__37;
mpz_t __gen_e_acsl_add_13;
- __gmpz_init_set_si(__gen_e_acsl__38,1L);
+ __gmpz_init_set_ui(__gen_e_acsl__37,1UL);
__gmpz_init(__gen_e_acsl_add_13);
__gmpz_add(__gen_e_acsl_add_13,
(__mpz_struct const *)(__gen_e_acsl_y_2),
- (__mpz_struct const *)(__gen_e_acsl__38));
+ (__mpz_struct const *)(__gen_e_acsl__37));
__gmpz_set(__gen_e_acsl_y_2,
(__mpz_struct const *)(__gen_e_acsl_add_13));
- __gmpz_clear(__gen_e_acsl__38);
+ __gmpz_clear(__gen_e_acsl__37);
__gmpz_clear(__gen_e_acsl_add_13);
}
}
@@ -545,8 +535,8 @@ int main(void)
__gen_e_acsl_implies = __gen_e_acsl_exists_2;
__gmpz_clear(__gen_e_acsl_y_2);
}
+ __gmpz_clear(__gen_e_acsl__31);
__gmpz_clear(__gen_e_acsl__32);
- __gmpz_clear(__gen_e_acsl__33);
__gmpz_clear(__gen_e_acsl_mod);
if (__gen_e_acsl_implies) ;
else {
@@ -555,16 +545,16 @@ int main(void)
}
}
{
- mpz_t __gen_e_acsl__41;
+ mpz_t __gen_e_acsl__39;
mpz_t __gen_e_acsl_add_14;
- __gmpz_init_set_si(__gen_e_acsl__41,1L);
+ __gmpz_init_set_ui(__gen_e_acsl__39,1UL);
__gmpz_init(__gen_e_acsl_add_14);
__gmpz_add(__gen_e_acsl_add_14,
(__mpz_struct const *)(__gen_e_acsl_x_7),
- (__mpz_struct const *)(__gen_e_acsl__41));
+ (__mpz_struct const *)(__gen_e_acsl__39));
__gmpz_set(__gen_e_acsl_x_7,
(__mpz_struct const *)(__gen_e_acsl_add_14));
- __gmpz_clear(__gen_e_acsl__41);
+ __gmpz_clear(__gen_e_acsl__39);
__gmpz_clear(__gen_e_acsl_add_14);
}
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
index 1c898816ecc..9a921a8df6a 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
@@ -12,7 +12,7 @@
__e_acsl_heap_size ∈ [--..--]
tests/gmp/quantif.i:9:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_init
-[value] using specification for function __gmpz_init_set_si
+[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_set
[value] using specification for function __gmpz_clear
tests/gmp/quantif.i:9:[value] entering loop for the first time
@@ -29,6 +29,7 @@ tests/gmp/quantif.i:12:[value] entering loop for the first time
tests/gmp/quantif.i:16:[value] warning: assertion got status unknown.
tests/gmp/quantif.i:16:[value] entering loop for the first time
tests/gmp/quantif.i:21:[value] warning: assertion got status unknown.
+[value] using specification for function __gmpz_set_si
tests/gmp/quantif.i:21:[value] entering loop for the first time
tests/gmp/quantif.i:25:[value] warning: assertion got status unknown.
tests/gmp/quantif.i:25:[value] entering loop for the first time
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 4588a8391ad..cafde44823e 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -151,6 +151,7 @@ let constant_to_exp ~loc t = function
raise Cil.Not_representable
| (None | Some _), _ -> Cil.kinteger64 ~loc ~kind ?repr n, false
with Cil.Not_representable ->
+
(* too big integer *)
Cil.mkString ~loc (Integer.to_string n), true)
| LStr s -> Cil.new_exp ~loc (Const (CStr s)), false
@@ -297,7 +298,7 @@ and context_insensitive_term_to_exp kf env t =
(* [!t] is converted into [t == 0] *)
let zero = Logic_const.tinteger 0 in
let ctx = Typing.get_integer_ty t in
- Typing.type_term ~ctx zero;
+ Typing.type_term ~force:false ~ctx zero;
let e, env =
comparison_to_exp kf ~loc ~name:"not" env Typing.gmp Eq t zero (Some t)
in
@@ -341,7 +342,7 @@ and context_insensitive_term_to_exp kf env t =
possible values of [t2] *)
(* guarding divisions and modulos *)
let zero = Logic_const.tinteger 0 in
- Typing.type_term ~ctx zero;
+ Typing.type_term ~force:false ~ctx zero;
(* do not generate [e2] from [t2] twice *)
let guard, env =
let name = name_of_binop bop ^ "_guard" in
@@ -805,7 +806,7 @@ let term_to_exp typ t =
| TInt(ik, _) -> Typing.ikind ik
| _ -> Typing.c_int (* useless, but required *)
in
- Typing.type_term ~ctx t;
+ Typing.type_term ~force:false ~ctx t;
let env = Env.empty (new Visitor.frama_c_copy Project_skeleton.dummy) in
let env = Env.push env in
let env = Env.rte env false in
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 0144e50010c..b50e6c300c6 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -45,18 +45,21 @@ let gmp = Gmp
let c_int = C_type IInt
let ikind ik = C_type ik
-let join ty1 ty2 = match ty1, ty2 with
- | Other, Other -> Other
- | Other, (Gmp | C_type _) | (Gmp | C_type _), Other ->
- Options.fatal "[typing] join failure: integer and non integer type"
- | Gmp, _ | _, Gmp -> Gmp
- | C_type i1, C_type i2 ->
- let ty = Cil.arithmeticConversion (TInt(i1, [])) (TInt(i2, [])) in
- match ty with
- | TInt(i, _) -> C_type i
- | _ ->
- Options.fatal "[typing] join failure: unexpected result %a"
- Printer.pp_typ ty
+let join ty1 ty2 =
+ if Options.Gmp_only.get () then Gmp
+ else
+ match ty1, ty2 with
+ | Other, Other -> Other
+ | Other, (Gmp | C_type _) | (Gmp | C_type _), Other ->
+ Options.fatal "[typing] join failure: integer and non integer type"
+ | Gmp, _ | _, Gmp -> Gmp
+ | C_type i1, C_type i2 ->
+ let ty = Cil.arithmeticConversion (TInt(i1, [])) (TInt(i2, [])) in
+ match ty with
+ | TInt(i, _) -> C_type i
+ | _ ->
+ Options.fatal "[typing] join failure: unexpected result %a"
+ Printer.pp_typ ty
exception Not_an_integer
let typ_of_integer_ty = function
@@ -165,14 +168,14 @@ let coerce ~ctx ~op ty =
(** {2 Type system} *)
(******************************************************************************)
-let mk_ctx ?(force=false) c =
+let mk_ctx ~force c =
if force then c
else match c with
| Other -> Other
| Gmp | C_type _ -> if Options.Gmp_only.get () then Gmp else c
-let rec type_term env ?force ~ctx t =
- let ctx = mk_ctx ?force ctx in
+let rec type_term ~force ~ctx t =
+ let ctx = mk_ctx ~force ctx in
let dup ty = ty, ty in
let infer t =
Cil.CurrentLoc.set t.term_loc;
@@ -183,22 +186,21 @@ let rec type_term env ?force ~ctx t =
| TAlignOf _ ->
let ty =
try
- let i = Interval.infer env t in
+ let i = Interval.infer t in
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other
in
dup ty
-
| TLval tlv ->
let ty =
try
- let i = Interval.infer env t in
+ let i = Interval.infer t in
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other
in
- type_term_lval env tlv;
+ type_term_lval tlv;
dup ty
| Toffset(_, t')
@@ -207,9 +209,9 @@ let rec type_term env ?force ~ctx t =
| TAlignOfE t' ->
let ty =
try
- let i = Interval.infer env t in
+ let i = Interval.infer t in
(* [t'] must be typed, but it is a pointer *)
- ignore (type_term env ~ctx:Other t');
+ ignore (type_term ~force:false ~ctx:Other t');
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
assert false
@@ -219,10 +221,10 @@ let rec type_term env ?force ~ctx t =
| TBinOp (MinusPP, t1, t2) ->
let ty =
try
- let i = Interval.infer env t in
+ let i = Interval.infer t in
(* [t1] and [t2] must be typed, but they are pointers *)
- ignore (type_term env ~ctx:Other t1);
- ignore (type_term env ~ctx:Other t2);
+ ignore (type_term ~force:false ~ctx:Other t1);
+ ignore (type_term ~force:false ~ctx:Other t2);
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
assert false
@@ -232,13 +234,13 @@ let rec type_term env ?force ~ctx t =
| TUnOp (unop, t') ->
let ctx =
try
- let i = Interval.infer env t in
- let i' = Interval.infer env t' in
- mk_ctx (ty_of_interv ~ctx (Interval.join i i'))
+ let i = Interval.infer t in
+ let i' = Interval.infer t' in
+ mk_ctx ~force:false (ty_of_interv ~ctx (Interval.join i i'))
with Interval.Not_an_integer ->
Other (* real *)
in
- ignore (type_term env ~ctx t');
+ ignore (type_term ~force:false ~ctx t');
(match unop with
| LNot -> c_int, ctx (* converted into [t == 0] in casse of GMP *)
| Neg | BNot -> dup ctx)
@@ -246,29 +248,30 @@ let rec type_term env ?force ~ctx t =
| TBinOp((PlusA | MinusA | Mult | Div | Mod | Shiftlt | Shiftrt), t1, t2) ->
let ctx =
try
- let i = Interval.infer env t in
- let i1 = Interval.infer env t1 in
- let i2 = Interval.infer env t2 in
- mk_ctx (ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2)))
+ let i = Interval.infer t in
+ let i1 = Interval.infer t1 in
+ let i2 = Interval.infer t2 in
+ let ctx = ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2)) in
+ mk_ctx ~force:false ctx
with Interval.Not_an_integer ->
Other (* real *)
in
- ignore (type_term env ~ctx t1);
- ignore (type_term env ~ctx t2);
+ ignore (type_term ~force ~ctx t1);
+ ignore (type_term ~force ~ctx t2);
dup ctx
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
assert (compare ctx c_int >= 0);
let ctx =
try
- let i1 = Interval.infer env t1 in
- let i2 = Interval.infer env t2 in
- mk_ctx (ty_of_interv ~ctx (Interval.join i1 i2))
+ let i1 = Interval.infer t1 in
+ let i2 = Interval.infer t2 in
+ mk_ctx ~force:false (ty_of_interv ~ctx (Interval.join i1 i2))
with Interval.Not_an_integer ->
Other
in
- ignore (type_term env ~ctx t1);
- ignore (type_term env ~ctx t2);
+ ignore (type_term ~force:false ~ctx t1);
+ ignore (type_term ~force:false ~ctx t2);
let ty = match ctx with
| Other -> c_int
| Gmp | C_type _ -> ctx
@@ -278,15 +281,15 @@ let rec type_term env ?force ~ctx t =
| TBinOp ((LAnd | LOr), t1, t2) ->
let ty =
try
- let i1 = Interval.infer env t1 in
- let i2 = Interval.infer env t2 in
+ let i1 = Interval.infer t1 in
+ let i2 = Interval.infer t2 in
ty_of_interv ~ctx (Interval.join i1 i2)
with Interval.Not_an_integer ->
Other
in
(* both operands fit in an int. *)
- ignore (type_term env ~ctx:c_int t1);
- ignore (type_term env ~ctx:c_int t2);
+ ignore (type_term ~force:false ~ctx:c_int t1);
+ ignore (type_term ~force:false ~ctx:c_int t2);
dup ty
| TBinOp (BAnd, _, _) -> Error.not_yet "bitwise and"
@@ -297,7 +300,7 @@ let rec type_term env ?force ~ctx t =
| TCoerce(t', _) ->
let ctx =
try
- let i = Interval.infer env t' in
+ let i = Interval.infer t' in
(* nothing more to do: [i] is already more precise than what we
could infer from the arguments of the cast. Also, do not type the
internal term: possibly it is not even an integer *)
@@ -305,58 +308,59 @@ let rec type_term env ?force ~ctx t =
with Interval.Not_an_integer ->
Other
in
- ignore (type_term env ~ctx t');
+ ignore (type_term ~force:false ~ctx t');
dup ctx
| Tif (t1, t2, t3) ->
- let ctx = mk_ctx c_int in
- ignore (type_term env ~ctx t1);
- let i = Interval.infer env t in
+ let ctx1 = mk_ctx ~force:true c_int in
+ ignore (type_term ~force:true ~ctx:ctx1 t1);
+ let i = Interval.infer t in
let ctx =
try
- let i2 = Interval.infer env t2 in
- let i3 = Interval.infer env t3 in
- mk_ctx (ty_of_interv ~ctx (Interval.join i (Interval.join i2 i3)))
+ let i2 = Interval.infer t2 in
+ let i3 = Interval.infer t3 in
+ let ctx = ty_of_interv ~ctx (Interval.join i (Interval.join i2 i3)) in
+ mk_ctx ~force:false ctx
with Interval.Not_an_integer ->
Other
in
- ignore (type_term env ~ctx t2);
- ignore (type_term env ~ctx t3);
+ ignore (type_term ~force:false ~ctx t2);
+ ignore (type_term ~force:false ~ctx t3);
dup ctx
| Tat (t, _)
- | TLogic_coerce (_, t) -> dup (type_term env ~ctx t).ty
+ | TLogic_coerce (_, t) -> dup (type_term ~force:false ~ctx t).ty
| TCoerceE (t1, t2) ->
let ctx =
try
- let i = Interval.infer env t in
- let i1 = Interval.infer env t1 in
- let i2 = Interval.infer env t2 in
+ let i = Interval.infer t in
+ let i1 = Interval.infer t1 in
+ let i2 = Interval.infer t2 in
ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2))
with Interval.Not_an_integer ->
Other
in
- ignore (type_term env ~ctx t1);
- ignore (type_term env ~ctx t2);
+ ignore (type_term ~force:true ~ctx t1);
+ ignore (type_term ~force:true ~ctx t2);
dup ctx
| TAddrOf tlv
| TStartOf tlv ->
(* it is a pointer, as well as [t], but [t] must be typed. *)
- type_term_lval env tlv;
+ type_term_lval tlv;
dup Other
| Tbase_addr (_, t) ->
(* it is a pointer, as well as [t], but [t] must be typed. *)
- ignore (type_term env ~ctx:Other t);
+ ignore (type_term ~force:false ~ctx:Other t);
dup Other
| TBinOp ((PlusPI | IndexPI | MinusPI), t1, t2) ->
(* it is a pointer, as well as [t1], while [t2] is a size_t.
Both [t1] and [t2] must be typed. *)
- ignore (type_term env ~ctx:Other t1);
- ignore (type_term env ~force:true ~ctx:(size_t ()) t2);
+ ignore (type_term ~force:false ~ctx:Other t1);
+ ignore (type_term ~force:true ~ctx:(size_t ()) t2);
dup Other
| Tapp (_,_,_) -> Error.not_yet "logic function application"
@@ -377,25 +381,25 @@ let rec type_term env ?force ~ctx t =
in
Memo.memo (fun t -> let ty, op = infer t in coerce ~ctx ~op ty) t
-and type_term_lval env (host, offset) =
- type_term_lhost env host;
- type_term_offset env offset
+and type_term_lval (host, offset) =
+ type_term_lhost host;
+ type_term_offset offset
-and type_term_lhost env = function
+and type_term_lhost = function
| TVar _
| TResult _ -> ()
- | TMem t -> ignore (type_term env ~ctx:Other t)
+ | TMem t -> ignore (type_term ~force:false ~ctx:Other t)
-and type_term_offset env = function
+and type_term_offset = function
| TNoOffset -> ()
| TField(_, toff)
- | TModel(_, toff) -> type_term_offset env toff
+ | TModel(_, toff) -> type_term_offset toff
| TIndex(t, toff) ->
- (* [t] is an array index which must fits into size_t *)
- ignore (type_term env ~force:true ~ctx:(size_t ()) t);
- type_term_offset env toff
+ (* [t] is an array index which must fit into size_t *)
+ ignore (type_term ~force:true ~ctx:(size_t ()) t);
+ type_term_offset toff
-let rec type_predicate_named env p =
+let rec type_predicate_named p =
Cil.CurrentLoc.set p.loc;
let op = match p.content with
| Pfalse | Ptrue -> c_int
@@ -405,15 +409,15 @@ let rec type_predicate_named env p =
| Prel(_, t1, t2) ->
let ctx =
try
- let i1 = Interval.infer env t1 in
- let i2 = Interval.infer env t2 in
+ let i1 = Interval.infer t1 in
+ let i2 = Interval.infer t2 in
let i = Interval.join i1 i2 in
- mk_ctx (ty_of_interv ~ctx:c_int i)
+ mk_ctx ~force:false (ty_of_interv ~ctx:c_int i)
with Interval.Not_an_integer ->
Other
in
- ignore (type_term env ~ctx t1);
- ignore (type_term env ~ctx t2);
+ ignore (type_term ~force:false ~ctx t1);
+ ignore (type_term ~force:false ~ctx t2);
(match ctx with
| Other -> c_int
| Gmp | C_type _ -> ctx)
@@ -422,62 +426,59 @@ let rec type_predicate_named env p =
| Pxor(p1, p2)
| Pimplies(p1, p2)
| Piff(p1, p2) ->
- ignore (type_predicate_named env p1);
- ignore (type_predicate_named env p2);
+ ignore (type_predicate_named p1);
+ ignore (type_predicate_named p2);
c_int
| Pnot p ->
- ignore (type_predicate_named env p);
+ ignore (type_predicate_named p);
c_int
| Pif(t, p1, p2) ->
- let ctx = mk_ctx c_int in
- ignore (type_term env ~ctx t);
- ignore (type_predicate_named env p1);
- ignore (type_predicate_named env p2);
+ let ctx = mk_ctx ~force:true c_int in
+ ignore (type_term ~force:true ~ctx t);
+ ignore (type_predicate_named p1);
+ ignore (type_predicate_named p2);
c_int
| Plet _ -> Error.not_yet "let _ = _ in _"
+
| Pforall(bounded_vars, { content = Pimplies(hyps, goal) })
| Pexists(bounded_vars, { content = Pand(hyps, goal) }) ->
let guards = !compute_quantif_guards_ref p bounded_vars hyps in
- let env =
- List.fold_left
- (fun env (t1, r1, x, r2, t2) ->
- let i1 = Interval.infer env t1 in
- let i1 = match r1 with
- | Rlt -> Interval.add i1 Integer.one
- | Rle -> i1
- | _ -> assert false
- in
- let i2 = Interval.infer env t2 in
+ List.iter
+ (fun (t1, r1, x, r2, t2) ->
+ let i1 = Interval.infer t1 in
+ let i1 = match r1 with
+ | Rlt -> Interval.add i1 Integer.one
+ | Rle -> i1
+ | _ -> assert false
+ in
+ let i2 = Interval.infer t2 in
(* add one to [i2], since we increment the loop counter one more
- time before going out the loop. *)
- let i2 = match r2 with
- | Rlt -> i2
- | Rle -> Interval.add i2 Integer.one
- | _ -> assert false
- in
- let i = Interval.join i1 i2 in
- let ctx = match x.lv_type with
- | Linteger -> Gmp
- | Ctype ty ->
- (match Cil.unrollType ty with
- | TInt(ik, _) -> C_type ik
- | ty ->
- Options.fatal "unexpected type %a for quantified variable %a"
- Printer.pp_typ ty
- Printer.pp_logic_var x)
- | lty ->
+ time before going outside the loop. *)
+ let i2 = match r2 with
+ | Rlt -> i2
+ | Rle -> Interval.add i2 Integer.one
+ | _ -> assert false
+ in
+ let i = Interval.join i1 i2 in
+ let ctx = match x.lv_type with
+ | Linteger -> mk_ctx ~force:false (ty_of_interv ~ctx:Gmp i)
+ | Ctype ty ->
+ (match Cil.unrollType ty with
+ | TInt(ik, _) -> C_type ik
+ | ty ->
Options.fatal "unexpected type %a for quantified variable %a"
- Printer.pp_logic_type lty
- Printer.pp_logic_var x
- in
- let ctx = mk_ctx (ty_of_interv ~ctx i) in
- ignore (type_term env ~ctx t1);
- ignore (type_term env ~ctx t2);
- Interval.Env.add x i env)
- env
- guards
- in
- (type_predicate_named env goal).ty
+ Printer.pp_typ ty
+ Printer.pp_logic_var x)
+ | lty ->
+ Options.fatal "unexpected type %a for quantified variable %a"
+ Printer.pp_logic_type lty
+ Printer.pp_logic_var x
+ in
+ ignore (type_term ~force:true ~ctx t1);
+ ignore (type_term ~force:true ~ctx t2);
+ Interval.Env.add x i)
+ guards;
+ (type_predicate_named goal).ty
| Pinitialized(_, t)
| Pfreeable(_, t)
@@ -485,27 +486,30 @@ let rec type_predicate_named env p =
| Pvalid(_, t)
| Pvalid_read(_, t)
| Pvalid_function t ->
- ignore (type_term env ~ctx:Other t);
+ ignore (type_term ~force:false ~ctx:Other t);
c_int
| Pforall _ -> Error.not_yet "unguarded \\forall quantification"
| Pexists _ -> Error.not_yet "unguarded \\exists quantification"
- | Pat(p, _) -> (type_predicate_named env p).ty
+ | Pat(p, _) -> (type_predicate_named p).ty
| Pfresh _ -> Error.not_yet "\\fresh"
| Psubtype _ -> Error.not_yet "subtyping relation" (* Jessie specific *)
in
coerce ~ctx:c_int ~op c_int
-let type_term ~ctx t =
+let type_term ~force ~ctx t =
Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
Printer.pp_term t pretty ctx;
- ignore (type_term Interval.Env.empty ~ctx t)
+ ignore (type_term ~force ~ctx t)
let type_named_predicate ?(must_clear=true) p =
Options.feedback ~dkey ~level:3 "typing predicate '%a'."
Printer.pp_predicate_named p;
- if must_clear then Memo.clear ();
- ignore (type_predicate_named Interval.Env.empty p)
+ if must_clear then begin
+ Interval.Env.clear ();
+ Memo.clear ()
+ end;
+ ignore (type_predicate_named p)
(******************************************************************************)
(** {2 Getters} *)
@@ -513,17 +517,19 @@ let type_named_predicate ?(must_clear=true) p =
let get_integer_ty t = (Memo.get t).ty
let get_integer_op t = (Memo.get t).op
-
-let get_integer_op_of_predicate p =
- (type_predicate_named Interval.Env.empty (* the env is useless *) p).op
+let get_integer_op_of_predicate p = (type_predicate_named p).op
let extract_typ t ty =
try typ_of_integer_ty ty
with Not_an_integer ->
- let ty = t.term_type in
- if Cil.isLogicRealType ty then TFloat(FLongDouble, [])
- else if Cil.isLogicFloatType ty then Logic_utils.logicCType ty
- else assert false
+ let lty = t.term_type in
+ if Cil.isLogicRealType lty then TFloat(FLongDouble, [])
+ else if Cil.isLogicFloatType lty then Logic_utils.logicCType lty
+ else
+ Kernel.fatal "unexpected types %a and %a for term %a"
+ Printer.pp_logic_type lty
+ pretty ty
+ Printer.pp_term t
let get_typ t =
let info = Memo.get t in
@@ -540,8 +546,7 @@ let get_cast t =
with Not_an_integer -> None
let get_cast_of_predicate p =
- (* the env is useless *)
- let info = type_predicate_named Interval.Env.empty p in
+ let info = type_predicate_named p in
try Extlib.opt_map typ_of_integer_ty info.cast
with Not_an_integer -> assert false
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 93b80b960c4..2d90b0ec691 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -35,6 +35,8 @@ type integer_ty = private
| C_type of ikind
| Other
+include Datatype.S with type t = integer_ty
+
val gmp: integer_ty
val c_int: integer_ty
val ikind: ikind -> integer_ty
@@ -47,8 +49,10 @@ val join: integer_ty -> integer_ty -> integer_ty
(** {2 Typing} *)
(******************************************************************************)
-val type_term: ctx:integer_ty -> term -> unit
-(** Compute the type of each subterm of the given term. *)
+val type_term: force:bool -> ctx:integer_ty -> term -> unit
+(** Compute the type of each subterm of the given term in the given context. If
+ [force] is true, then the conversion to the given context is done even if
+ -e-acsl-gmp-only is set. *)
val type_named_predicate: ?must_clear:bool -> predicate named -> unit
(** Compute the type of each term of the given predicate. *)
--
GitLab