From 6ac06792d1c20abf78bbce1f6f5e9d4d014db128 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 9 Jul 2019 11:21:43 +0200
Subject: [PATCH] [Eva] Eval_terms: fully supports is_plus_infinity and
is_minus_infinity.
---
src/plugins/value/legacy/eval_terms.ml | 15 +++++++++++++++
1 file changed, 15 insertions(+)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index c40ad9050fd..3cddc2d8175 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -640,6 +640,8 @@ let known_logic_funs = [
let known_predicates = [
"\\warning", ACSL;
"\\is_finite", ACSL;
+ "\\is_plus_infinity", ACSL;
+ "\\is_minus_infinity", ACSL;
"\\is_NaN", ACSL;
"\\eq_float", ACSL;
"\\ne_float", ACSL;
@@ -1788,9 +1790,22 @@ let reduce_by_known_papp ~alarm_mode env positive li _labels args =
with LogicEvalError _ | Not_an_exact_loc | Cvalue.V.Not_based_on_null ->
env
in
+ let reduce_by_infinity ~pos prec f =
+ let inf = if pos then Fval.pos_infinity prec else Fval.neg_infinity prec in
+ let fval =
+ if positive
+ then inf
+ else Fval.(join nan (join (Fval.neg inf) (top_finite prec)))
+ in
+ Fval.narrow fval f
+ in
match positive, li.l_var_info.lv_name, args with
| _, "\\is_finite", [arg] ->
reduce_float (Fval.backward_is_finite ~positive) arg
+ | _, "\\is_plus_infinity", [arg] ->
+ reduce_float (reduce_by_infinity ~pos:true) arg
+ | _, "\\is_minus_infinity", [arg] ->
+ reduce_float (reduce_by_infinity ~pos:false) arg
| _, "\\is_NaN", [arg] ->
reduce_float (fun _fkind -> Fval.backward_is_nan ~positive) arg
| _ , ("\\eq_float" | "\\eq_double"), [t1;t2] ->
--
GitLab