From d3881b115cfc974bab3a43363c6ccaba9ad85c98 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 6 Sep 2019 10:24:04 +0200
Subject: [PATCH] [Eva] Removes an unused option and groups all options about
the traces domain.
---
src/plugins/value/value_parameters.ml | 52 +++++++++++---------------
src/plugins/value/value_parameters.mli | 11 +++---
2 files changed, 27 insertions(+), 36 deletions(-)
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index c51fb40570e..118115fa8b5 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -233,6 +233,13 @@ module SignDomain = Domain_Parameter
let default = false
end)
+module TracesDomain = Domain_Parameter
+ (struct
+ let option_name = "-eva-traces-domain"
+ let help = "Use a domain to record traces of Eva. Experimental."
+ let default = false
+ end)
+
module PrinterDomain = Domain_Parameter
(struct
let option_name = "-eva-printer-domain"
@@ -275,28 +282,6 @@ module EqualityCallFunction =
end)
let () = add_precision_dep EqualityCallFunction.parameter
-module TracesDomain = Domain_Parameter
- (struct
- let option_name = "-eva-traces-domain"
- let help = "Use a domain to record traces of Eva. Experimental."
- let default = false
- end)
-
-module TracesUnrollLoop = Domain_Parameter
- (struct
- let option_name = "-eva-traces-unroll-loop"
- let help = "Specify if the traces domain should unroll the loops."
- let default = true
- end)
-
-module TracesUnifyLoop = Domain_Parameter
- (struct
- let option_name = "-eva-traces-unify-loop"
- let help = "Specify if all the instances of a loop should try to share theirs traces."
- let default = false
- end)
-
-
let () = Parameter_customize.set_group domains
module Numerors_Real_Size =
Int
@@ -329,15 +314,25 @@ let () =
let () = add_precision_dep Numerors_Mode.parameter
let () = Parameter_customize.set_group domains
-module TracesStorage =
+module TracesUnrollLoop =
Bool
(struct
- let option_name = "-eva-traces-storage"
- let help = "Stores the states of the traces domain during the \
- analysis."
+ let option_name = "-eva-traces-unroll-loop"
+ let help = "Specify if the traces domain should unroll the loops."
let default = true
end)
-let () = add_precision_dep TracesStorage.parameter
+let () = add_precision_dep TracesUnrollLoop.parameter
+
+let () = Parameter_customize.set_group domains
+module TracesUnifyLoop =
+ Bool
+ (struct
+ let option_name = "-eva-traces-unify-loop"
+ let help = "Specify if all the instances of a loop should try \
+ to share theirs traces."
+ let default = false
+ end)
+let () = add_precision_dep TracesUnifyLoop.parameter
let () = Parameter_customize.set_group domains
module TracesDot = Empty_string
@@ -347,7 +342,6 @@ module TracesDot = Empty_string
let arg_name = "FILENAME"
end)
-
let () = Parameter_customize.set_group domains
module TracesProject = Bool
(struct
@@ -355,8 +349,6 @@ module TracesProject = Bool
let help = "Try to convert the Cfg into a program in a new project."
let default = false
end)
-let () = add_precision_dep TracesProject.parameter
-
(* -------------------------------------------------------------------------- *)
(* --- Performance options --- *)
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 5aa46bb0a03..dc958517ee4 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -38,8 +38,6 @@ module SignDomain: Parameter_sig.Bool
module PrinterDomain: Parameter_sig.Bool
module NumerorsDomain: Parameter_sig.Bool
module TracesDomain: Parameter_sig.Bool
-module TracesUnrollLoop: Parameter_sig.Bool
-module TracesUnifyLoop: Parameter_sig.Bool
module ApronOctagon: Parameter_sig.Bool
module ApronBox: Parameter_sig.Bool
@@ -52,15 +50,16 @@ module EqualityCallFunction:
Parameter_sig.Map with type key = Cil_types.kernel_function
and type value = string
+module TracesUnrollLoop: Parameter_sig.Bool
+module TracesUnifyLoop: Parameter_sig.Bool
+module TracesDot: Parameter_sig.String
+module TracesProject: Parameter_sig.Bool
+
module EqualityStorage: Parameter_sig.Bool
module SymbolicLocsStorage: Parameter_sig.Bool
module GaugesStorage: Parameter_sig.Bool
module ApronStorage: Parameter_sig.Bool
module BitwiseOffsmStorage: Parameter_sig.Bool
-module TracesStorage: Parameter_sig.Bool
-module TracesDot: Parameter_sig.String
-module TracesProject: Parameter_sig.Bool
-
module AutomaticContextMaxDepth: Parameter_sig.Int
module AutomaticContextMaxWidth: Parameter_sig.Int
--
GitLab