From 58bd23af79268c0702c0cbf2e142a2c3e7c5d3bc Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 19 Sep 2019 16:56:10 +0200
Subject: [PATCH] [Override Std] Lint
---
src/plugins/override_std/basic_blocks.ml | 8 ++++----
src/plugins/override_std/basic_blocks.mli | 2 +-
src/plugins/override_std/memcpy.ml | 6 +++---
src/plugins/override_std/options.ml | 20 ++++++++++----------
src/plugins/override_std/transform.ml | 4 ++--
src/plugins/override_std/transform.mli | 2 +-
6 files changed, 21 insertions(+), 21 deletions(-)
diff --git a/src/plugins/override_std/basic_blocks.ml b/src/plugins/override_std/basic_blocks.ml
index db2fa62e8f9..03456bd5299 100644
--- a/src/plugins/override_std/basic_blocks.ml
+++ b/src/plugins/override_std/basic_blocks.ml
@@ -62,7 +62,7 @@ let size_var t value = {
l_tparams = [];
l_labels = [];
l_profile = [];
- l_body = LBterm value;
+ l_body = LBterm value;
}
(** Features related to terms *)
@@ -71,11 +71,11 @@ let cvar_to_tvar vi = tvar (cvar_to_lvar vi)
let tminus ?loc t1 t2 =
let minus, typ = match t1.term_type, t2.term_type with
- | Ctype(t1), Ctype(t2) when Cil.isPointerType t1 && Cil.isPointerType t2 ->
+ | Ctype(t1), Ctype(t2) when Cil.isPointerType t1 && Cil.isPointerType t2 ->
MinusPP, Linteger
| Ctype(t), _ when Cil.isPointerType t ->
MinusPI, Ctype(t)
- | t, _ ->
+ | t, _ ->
MinusA, t
in
term ?loc (TBinOp(minus, t1, t2)) typ
@@ -137,4 +137,4 @@ let pcorrect_len_bytes ?loc t bytes_len =
let pseparated_memories ?loc p1 len1 p2 len2 =
let b1 = tbuffer_range ?loc p1 len1 in
let b2 = tbuffer_range ?loc p2 len2 in
- pseparated ?loc [ b1 ; b2 ]
\ No newline at end of file
+ pseparated ?loc [ b1 ; b2 ]
diff --git a/src/plugins/override_std/basic_blocks.mli b/src/plugins/override_std/basic_blocks.mli
index 95683f01d0b..396374230ce 100644
--- a/src/plugins/override_std/basic_blocks.mli
+++ b/src/plugins/override_std/basic_blocks.mli
@@ -45,4 +45,4 @@ val pcorrect_len_bytes: ?loc:location -> logic_type -> term -> predicate
val pseparated_memories: ?loc:location -> term -> term -> term -> term -> predicate
val plet_len_div_size:
- ?loc:location -> logic_type -> term -> (term -> predicate) -> predicate
\ No newline at end of file
+ ?loc:location -> logic_type -> term -> (term -> predicate) -> predicate
diff --git a/src/plugins/override_std/memcpy.ml b/src/plugins/override_std/memcpy.ml
index 0ca191c8860..d01b1d1ffa0 100644
--- a/src/plugins/override_std/memcpy.ml
+++ b/src/plugins/override_std/memcpy.ml
@@ -48,7 +48,7 @@ let pcopied_memcpy ?loc p1 p2 len =
let pcopied_len_bytes ?loc p1 p2 bytes_len =
plet_len_div_size ?loc p1.term_type bytes_len (pcopied_memcpy ?loc p1 p2)
-let generate_requires loc dest src len =
+let generate_requires loc dest src len =
List.map new_predicate [
{ (pcorrect_len_bytes ~loc dest.term_type len) with pred_name = ["aligned_end"] } ;
{ (pvalid_len_bytes ~loc here_label dest len) with pred_name = ["valid_dest"] } ;
@@ -62,7 +62,7 @@ let generate_assigns loc t dest src len =
let copy = dest_range, From [src_range] in
let result = new_identified_term (tresult t) in
let dest = new_identified_term dest in
- let res = result, From [dest] in
+ let res = result, From [dest] in
Writes [ copy ; res ]
let generate_ensures loc dest src len =
@@ -158,4 +158,4 @@ let () = Transform.register (module struct
let replace_call = replace_call
let get_globals = get_globals
let reset () = Hashtbl.reset table
- end)
\ No newline at end of file
+ end)
diff --git a/src/plugins/override_std/options.ml b/src/plugins/override_std/options.ml
index b52116a613b..2c10031bd38 100644
--- a/src/plugins/override_std/options.ml
+++ b/src/plugins/override_std/options.ml
@@ -24,16 +24,16 @@ let name = "Override Std"
let shortname = "override-std"
include Plugin.Register
- (struct
- let name = name
- let shortname = shortname
- let help = "Overrides standard library functions"
- end)
+ (struct
+ let name = name
+ let shortname = shortname
+ let help = "Overrides standard library functions"
+ end)
module Enabled = True
- (struct
- let option_name = "-override-std-perform"
- let help = ""
- end)
+ (struct
+ let option_name = "-override-std-perform"
+ let help = ""
+ end)
-let emitter = Emitter.create shortname [Emitter.Funspec] ~correctness:[] ~tuning:[]
\ No newline at end of file
+let emitter = Emitter.create shortname [Emitter.Funspec] ~correctness:[] ~tuning:[]
diff --git a/src/plugins/override_std/transform.ml b/src/plugins/override_std/transform.ml
index 1fd8c90224d..58890264a0c 100644
--- a/src/plugins/override_std/transform.ml
+++ b/src/plugins/override_std/transform.ml
@@ -48,7 +48,7 @@ let get_globals loc =
let called_function = function
| Call(_, { enode = Lval((Var fct), NoOffset) }, _, _)
| Local_init(_, ConsInit(fct, _, Plain_func), _) -> fct
- | _ -> assert false
+ | _ -> assert false
let called_function_name inst =
let fct = called_function inst in fct.vname
@@ -91,4 +91,4 @@ class visitor = object(_)
end
let transform file =
- Visitor.visitFramacFile (new visitor) file
\ No newline at end of file
+ Visitor.visitFramacFile (new visitor) file
diff --git a/src/plugins/override_std/transform.mli b/src/plugins/override_std/transform.mli
index dcf037b5b1a..c311010a09f 100644
--- a/src/plugins/override_std/transform.mli
+++ b/src/plugins/override_std/transform.mli
@@ -30,4 +30,4 @@ module type Override = sig
end
val register: (module Override) -> unit
-val transform: Cil_types.file -> unit
\ No newline at end of file
+val transform: Cil_types.file -> unit
--
GitLab