From c80b4dda7d4aeec42342d3505cd0011141aab79d Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Tue, 14 Jun 2022 14:10:52 +0200
Subject: [PATCH] [e-acsl] review
---
src/plugins/e-acsl/src/analyses/analyses_types.mli | 5 +++--
src/plugins/e-acsl/src/analyses/typing.ml | 2 +-
2 files changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/analyses_types.mli b/src/plugins/e-acsl/src/analyses/analyses_types.mli
index 4a00a6fa9a2..ea2ec78290d 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_types.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_types.mli
@@ -68,7 +68,7 @@ type annotation_kind =
| Variant
| RTE
-(** Type of intervals infered by the interval inference *)
+(** Type of intervals inferred by the interval inference *)
type ival =
| Ival of Ival.t
| Float of fkind * float option (* a float constant, if any *)
@@ -76,7 +76,8 @@ type ival =
| Real
| Nan
-(** Type of types infered by the type inference for types representing numbers *)
+(** Type of types inferred by the type inference for types representing
+ numbers *)
type number_ty =
| C_integer of ikind
| C_float of fkind
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 78f30377014..e005bcb1db7 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -423,7 +423,7 @@ let rec type_term
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
assert
(match ctx with
- |None -> true
+ | None -> true
| Some c -> Number_ty.compare c c_int >= 0);
let ctx = ctx_relation ~profile t1 t2 in
ignore (type_term ~use_gmp_opt:true ~ctx ~profile t1);
--
GitLab