From 1fdecff95d2d1b13660f02219ec13fe7cdc30e89 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 6 Jan 2020 13:52:17 +0100
Subject: [PATCH] [e-acsl] lint
---
src/plugins/e-acsl/src/analyses/typing.ml | 10 +++++-----
src/plugins/e-acsl/src/main.ml | 2 +-
.../e-acsl/src/project_initializer/prepare_ast.ml | 4 ++--
.../e-acsl/src/project_initializer/prepare_ast.mli | 2 +-
4 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index b59e1c17593..12ff23ceaff 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -191,11 +191,11 @@ end = struct
useless. However:
- type info of many terms are accessed several times
- the translation of E-ACSL guarded quantifications generates
- new terms (see module {!Quantif}) which must be typed. The term
- corresponding to the bound variable [x] is actually used twice: once in the
- guard and once for encoding [x+1] when incrementing it. The memoization is
- only useful here and indeed prevent the generation of one extra variable in
- some cases. *)
+ new terms (see module {!Quantif}) which must be typed. The term
+ corresponding to the bound variable [x] is actually used twice: once in the
+ guard and once for encoding [x+1] when incrementing it. The memoization is
+ only useful here and indeed prevent the generation of one extra variable in
+ some cases. *)
let tbl = Misc.Id_term.Hashtbl.create 97
let get t =
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index c7546057321..99b4c04db36 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -158,7 +158,7 @@ let generate_code =
Options.feedback "translation done in project \"%s\"."
(Options.Project_name.get ());
copied_prj)
-())
+ ())
let generate_code =
Dynamic.register
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index cf20d89e609..a0ba3f2b740 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -245,9 +245,9 @@ let align_error s = raise (Alignment_error s)
of [algn] or greater. Returns false otherwise.
Throws an exception if
- [attrs] contains several [align] attributes specifying different
- alignments
+ alignments
- [attrs] has a single align attribute with a value which is less than
- [algn] *)
+ [algn] *)
let sufficiently_aligned attrs algn =
let alignment =
List.fold_left
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
index f9739a57ffa..d09c270d2ae 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
@@ -29,7 +29,7 @@
statements to upper scopes;
- storing what is necessary to translate in [Keep_status]
- in case of temporal validity checks, adding the attribute "aligned" to
- variables that are not sufficiently aligned. *)
+ variables that are not sufficiently aligned. *)
val prepare: unit -> unit
--
GitLab