Commit 1fdecff9 authored by Julien Signoles's avatar Julien Signoles

[e-acsl] lint

parent 29d304c2
...@@ -191,11 +191,11 @@ end = struct ...@@ -191,11 +191,11 @@ end = struct
useless. However: useless. However:
- type info of many terms are accessed several times - type info of many terms are accessed several times
- the translation of E-ACSL guarded quantifications generates - the translation of E-ACSL guarded quantifications generates
new terms (see module {!Quantif}) which must be typed. The term new terms (see module {!Quantif}) which must be typed. The term
corresponding to the bound variable [x] is actually used twice: once in the 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 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 only useful here and indeed prevent the generation of one extra variable in
some cases. *) some cases. *)
let tbl = Misc.Id_term.Hashtbl.create 97 let tbl = Misc.Id_term.Hashtbl.create 97
let get t = let get t =
......
...@@ -158,7 +158,7 @@ let generate_code = ...@@ -158,7 +158,7 @@ let generate_code =
Options.feedback "translation done in project \"%s\"." Options.feedback "translation done in project \"%s\"."
(Options.Project_name.get ()); (Options.Project_name.get ());
copied_prj) copied_prj)
()) ())
let generate_code = let generate_code =
Dynamic.register Dynamic.register
......
...@@ -245,9 +245,9 @@ let align_error s = raise (Alignment_error s) ...@@ -245,9 +245,9 @@ let align_error s = raise (Alignment_error s)
of [algn] or greater. Returns false otherwise. of [algn] or greater. Returns false otherwise.
Throws an exception if Throws an exception if
- [attrs] contains several [align] attributes specifying different - [attrs] contains several [align] attributes specifying different
alignments alignments
- [attrs] has a single align attribute with a value which is less than - [attrs] has a single align attribute with a value which is less than
[algn] *) [algn] *)
let sufficiently_aligned attrs algn = let sufficiently_aligned attrs algn =
let alignment = let alignment =
List.fold_left List.fold_left
......
...@@ -29,7 +29,7 @@ ...@@ -29,7 +29,7 @@
statements to upper scopes; statements to upper scopes;
- storing what is necessary to translate in [Keep_status] - storing what is necessary to translate in [Keep_status]
- in case of temporal validity checks, adding the attribute "aligned" to - 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 val prepare: unit -> unit
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment