From a14aaeaf90124694e643dcd7d60b6ce8936d68b8 Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Wed, 13 Oct 2021 11:45:58 +0200
Subject: [PATCH] [e-acsl] minor corrections
---
src/plugins/e-acsl/headers/header_spec.txt | 4 ++--
src/plugins/e-acsl/src/analyses/typing.ml | 4 ++--
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index b8d2e280542..3daf5993839 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -76,8 +76,8 @@ src/analyses/interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/interval.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/literal_strings.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/literal_strings.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/predicate_normalizer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/predicate_normalizer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/logic_normalizer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/logic_normalizer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/lscope.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/lscope.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/memory_tracking.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 95c9189b0e6..bbc74b118c6 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -416,8 +416,8 @@ let rec type_term
| TSizeOfStr _
| TAlignOf _ ->
let i = Interval.infer t in
- (* a constant or an left value directly under a lambda should be a gmp
- if the infered context for the lambda is gmp *)
+ (* a constant or a left value directly under a lambda should be a gmp
+ if the infered context for the lambda is gmp *)
let ty = ty_of_interv ?ctx ~use_gmp_opt:under_lambda i in
dup ty
--
GitLab