From afae560037fb15a91e44acc19c0a144617cccb53 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 3 Apr 2020 13:50:09 +0200
Subject: [PATCH] [Instantiate] Lint
---
src/plugins/instantiate/global_context.ml | 2 +-
src/plugins/instantiate/global_context.mli | 6 +++---
src/plugins/instantiate/stdlib/basic_alloc.ml | 2 +-
3 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/plugins/instantiate/global_context.ml b/src/plugins/instantiate/global_context.ml
index 9a6d4ff32d6..9791a78d529 100644
--- a/src/plugins/instantiate/global_context.ml
+++ b/src/plugins/instantiate/global_context.ml
@@ -87,4 +87,4 @@ let globals loc =
let axiomatic name list loc = annot(Daxiomatic(name, list, [], loc)) loc in
let l = Table.fold (fun _ x l -> fun_or_pred x loc :: l) logic_functions l in
let l = Table.fold (fun n x l -> axiomatic n x loc :: l) axiomatics l in
- l
\ No newline at end of file
+ l
diff --git a/src/plugins/instantiate/global_context.mli b/src/plugins/instantiate/global_context.mli
index 89f3a212449..9a1456ff0bb 100644
--- a/src/plugins/instantiate/global_context.mli
+++ b/src/plugins/instantiate/global_context.mli
@@ -54,9 +54,9 @@ val get_logic_function: string -> (unit -> logic_info) -> logic_info
Note that function overloading is not supported.
*)
val get_logic_function_in_axiomatic:
- string ->
- (unit -> (string * global_annotation list) * logic_info list) ->
- logic_info
+ string ->
+ (unit -> (string * global_annotation list) * logic_info list) ->
+ logic_info
(** Clears internal tables *)
val clear: unit -> unit
diff --git a/src/plugins/instantiate/stdlib/basic_alloc.ml b/src/plugins/instantiate/stdlib/basic_alloc.ml
index 3f9ced7c231..a35a97b53e3 100644
--- a/src/plugins/instantiate/stdlib/basic_alloc.ml
+++ b/src/plugins/instantiate/stdlib/basic_alloc.ml
@@ -76,7 +76,7 @@ let make_axiomatic_is_allocable loc () =
let max =
tinteger
(Integer.to_int
- (Cil.max_unsigned_number (Cil.bitsSizeOf (size_t ()))))
+ (Cil.max_unsigned_number (Cil.bitsSizeOf (size_t ()))))
in
let label = FormalLabel("L") in
let cond = pand (prel (Rlt, t_i, zero), prel (Rgt, t_i, max)) in
--
GitLab