From a3084f08b07b1a6eba37a1e2c668bddc12f3f6c5 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 23 Aug 2019 18:02:49 +0200
Subject: [PATCH] [translate] add a few assertions
---
src/plugins/e-acsl/translate.ml | 46 +++++++++++++++------------------
1 file changed, 21 insertions(+), 25 deletions(-)
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index a969738ea00..1aaf8e0276f 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -210,8 +210,8 @@ let conditional_to_exp ?(name="if") loc t_opt e1 (e2, env2) (e3, env3) =
let lv = Cil.var v in
let ty = Cil.typeOf ev in
let init_set =
- (* TODO RATIONAL: how is it possible to get a real here? *)
- if Real.is_t ty then Real.init_set else Gmp.init_set
+ assert (not (Real.is_t ty));
+ Gmp.init_set
in
let affect e = init_set ~loc lv ev e in
let then_block, _ =
@@ -340,12 +340,10 @@ and context_insensitive_term_to_exp kf env t =
else if Real.is_t ty then
let e, env = Real.binop ~loc bop e1 e2 env (Some t) in
e, env, C_number, ""
- else
- if Logic_typing.is_integral_type t.term_type then
+ else begin
+ assert (Logic_typing.is_integral_type t.term_type);
Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, C_number, ""
- else
- (* TODO RATIONAL: why question mark? *)
- not_yet env "floating-point context (?)"
+ end
| TBinOp(Div | Mod as bop, t1, t2) ->
let ty = Typing.get_typ t in
let e1, env = term_to_exp kf env t1 in
@@ -368,19 +366,19 @@ and context_insensitive_term_to_exp kf env t =
~loc kf env Typing.gmpz ~e1:e2 ~name Eq t2 zero t
in
let mk_stmts _v e =
- assert (Gmp.Z.is_t ty);
- let vis = Env.get_visitor env in
- let kf = Extlib.the vis#current_kf in
- let cond =
- Misc.mk_e_acsl_guard
- (Env.annotation_kind env)
- kf
- guard
- (Logic_const.prel ~loc (Req, t2, zero))
- in
- Env.add_assert env cond (Logic_const.prel (Rneq, t2, zero));
- let instr = Misc.mk_call ~loc name [ e; e1; e2 ] in
- [ cond; instr ]
+ assert (Gmp.Z.is_t ty);
+ let vis = Env.get_visitor env in
+ let kf = Extlib.the vis#current_kf in
+ let cond =
+ Misc.mk_e_acsl_guard
+ (Env.annotation_kind env)
+ kf
+ guard
+ (Logic_const.prel ~loc (Req, t2, zero))
+ in
+ Env.add_assert env cond (Logic_const.prel (Rneq, t2, zero));
+ let instr = Misc.mk_call ~loc name [ e; e1; e2 ] in
+ [ cond; instr ]
in
let name = Misc.name_of_binop bop in
let _, e, env = Env.new_var_and_mpz_init ~loc ~name env t mk_stmts in
@@ -388,13 +386,11 @@ and context_insensitive_term_to_exp kf env t =
else if Real.is_t ty then
let e, env = Real.binop ~loc bop e1 e2 env (Some t) in
e, env, C_number, ""
- else
+ else begin
+ assert (Logic_typing.is_integral_type t.term_type);
(* no guard required since RTEs are generated separately *)
- if Logic_typing.is_integral_type t.term_type then
Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, C_number, ""
- else
- (* TODO RATIONAL: why question mark? *)
- not_yet env "floating-point context (?)"
+ end
| TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
(* comparison operators *)
let ity = Typing.get_integer_op t in
--
GitLab