From 83de5fb0fea120a48a5e2ce65fd33b8d6c7a0ed1 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 7 Oct 2019 11:49:41 +0200
Subject: [PATCH] [Eva] use singular form for octagon domain
---
doc/value/main.tex | 10 +++++-----
src/plugins/value/domains/octagons.ml | 10 +++++-----
src/plugins/value/engine/abstractions.ml | 2 +-
src/plugins/value/engine/abstractions.mli | 2 +-
src/plugins/value/value_parameters.ml | 22 +++++++++++-----------
src/plugins/value/value_parameters.mli | 4 ++--
tests/builtins/test_config_octagons | 2 +-
tests/test_config_octagons | 2 +-
tests/value/octagons.c | 8 ++++----
9 files changed, 31 insertions(+), 31 deletions(-)
diff --git a/doc/value/main.tex b/doc/value/main.tex
index 32076d0defe..2cc8c362d51 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -3960,7 +3960,7 @@ and \texttt{y} is not affine.
\subsection{Octagons}
\label{sec:octagons}
-Activating option \texttt{-eva-octagons-domain} instructs Eva to infer relations
+Activating option \texttt{-eva-octagon-domain} instructs Eva to infer relations
between variables as numerical constraints of the form $l \leq \pm X \pm Y \leq
u$, where $X$ and $Y$ are program variables, and $l$ and $u$ are constants.
@@ -3969,7 +3969,7 @@ of an expression involving $X$ and $Y$, or to deduce a reduction of
the possible values of $X$ from a reduction of the possible values of $Y$.
The following code is a minimal working example that illustrates
-the precision improvement provided by the octagons domain.
+the precision improvement provided by the octagon domain.
\begin{lstlisting}
void main (int y) {
int k = Frama_C_interval(0, 10);
@@ -3982,7 +3982,7 @@ void main (int y) {
\end{lstlisting}
-Currently, the octagons domain is fast but has two strong limitations:
+Currently, the octagon domain is fast but has two strong limitations:
\begin{itemize}
\item
The domain only infers relations between scalar variables of integer types.
@@ -3998,7 +3998,7 @@ The domain is intraprocedural by default: the inferred relations are local to
the current function and are lost when entering a function call or returning
to its caller.
-The option \verb+-eva-octagons-through-calls+ makes the octagons domain
+The option \verb+-eva-octagon-through-calls+ makes the octagon domain
interprocedural, which is a more precise but slower mode where
the inferred relations are propagated through function calls.
The analysis of a function can then use the relations inferred in the callers,
@@ -5093,7 +5093,7 @@ of the domain, shown in Figure~\ref{fig:log-category}.
Gauges & \lstinline|d-gauges| & \ref{sec:gauges}
\tabularnewline
\midrule
- Octagons & \lstinline|d-octagons| & \ref{sec:octagons}
+ Octagons & \lstinline|d-octagon| & \ref{sec:octagons}
\tabularnewline
\midrule
Bitwise & \lstinline|d-bitwise| & \ref{sec:bitwise}
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index aaaa686e582..f2b47bac5c7 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -38,11 +38,11 @@ let infer_intervals = true
minimal drop in efficiency. *)
let saturate_octagons = true
-(* Is the domain intraprocedural, according to the -eva-octagons-through-calls
+(* Is the domain intraprocedural, according to the -eva-octagon-through-calls
option. In this case, the analysis of each function starts with an empty
state, and the relations inferred in a function are not propagated back to
the caller either. *)
-let intraprocedural () = not (Value_parameters.OctagonsCall.get ())
+let intraprocedural () = not (Value_parameters.OctagonCall.get ())
(* -------------------------------------------------------------------------- *)
(* Basic types: pair of variables and Ival.t *)
@@ -420,7 +420,7 @@ end
while intervals for X+Y and X-Y shape a "leaning" rectangle; the intersection
of these rectangles shapes an octagon.
Using a misnomer, we call diamonds the intervals for X+Y and X-Y, and
- octagons the map from variables to diamonds, even if they does not exactly
+ octagons the maps from variables to diamonds, even if they do not exactly
shape octagons. *)
(* Relation between a pair of variables (X, Y).
@@ -777,7 +777,7 @@ module State = struct
then t
else
Value_parameters.abort
- "Incorrect octagons state computed by function %s:@ %a"
+ "Incorrect octagon state computed by function %s:@ %a"
msg pretty_debug t
(* ------------------------------ Lattice --------------------------------- *)
@@ -1315,7 +1315,7 @@ module Domain = struct
modified = current_input.modified }
let name = "Octagon domain"
- let log_category = Value_parameters.register_category "d-octagons"
+ let log_category = Value_parameters.register_category "d-octagon"
let storage () = true
end
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 3af8944a3a2..4261513ad85 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -98,7 +98,7 @@ module Config = struct
let cvalue = make 9 "cvalue" CvalueDomain.get (module Cvalue_domain.State)
let gauges = make 6 "gauges" GaugesDomain.get (module Gauges_domain.D)
- let octagons = make 6 "octagons" OctagonsDomain.get (module Octagons)
+ let octagon = make 6 "octagon" OctagonDomain.get (module Octagons)
let inout = make 5 "inout" InoutDomain.get (module Inout_domain.D)
let traces = make 2 "traces" TracesDomain.get (module Traces_domain.D)
let printer = make 2 "printer" PrinterDomain.get (module Printer_domain)
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index fe9179641e5..3d4ebe9e437 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -132,7 +132,7 @@ module Config : sig
val equality: flag
val symbolic_locations: flag
val gauges: flag
- val octagons: flag
+ val octagon: flag
val bitwise: flag
val inout: flag
val sign: flag
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 6061a2fef4b..0f972433fe4 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -167,10 +167,10 @@ module SymbolicLocsDomain = Domain_Parameter
let default = false
end)
-module OctagonsDomain = Domain_Parameter
+module OctagonDomain = Domain_Parameter
(struct
- let option_name = "-eva-octagons-domain"
- let help = "Use the octagons domain of Eva."
+ let option_name = "-eva-octagon-domain"
+ let help = "Use the octagon domain of Eva."
let default = false
end)
@@ -320,19 +320,19 @@ module EqualityCallFunction =
let () = add_precision_dep EqualityCallFunction.parameter
let () = Parameter_customize.set_group domains
-module OctagonsCall =
+module OctagonCall =
Bool
(struct
- let option_name = "-eva-octagons-through-calls"
- let help = "Whether the relations inferred by the octagons domain are \
+ let option_name = "-eva-octagon-through-calls"
+ let help = "Whether the relations inferred by the octagon domain are \
propagated through function calls. Disabled by default: \
- the octagons analysis is intra-procedural, starting \
- each function with an empty octagons state, \
+ the octagon analysis is intra-procedural, starting \
+ each function with an empty octagon state, \
and losing the octagons inferred at the end. \
The interprocedural analysis is more precise but slower."
let default = false
end)
-let () = add_precision_dep OctagonsCall.parameter
+let () = add_precision_dep OctagonCall.parameter
let () = Parameter_customize.set_group domains
module Numerors_Real_Size =
@@ -1542,8 +1542,8 @@ let () =
bind (module EqualityDomain) (fun n -> n > 1);
bind (module EqualityCall) (fun n -> if n > 2 then "formals" else "none");
bind (module GaugesDomain) (fun n -> n > 3);
- bind (module OctagonsDomain) (fun n -> n > 4);
- bind (module OctagonsCall) (fun n -> n > 5);
+ bind (module OctagonDomain) (fun n -> n > 4);
+ bind (module OctagonCall) (fun n -> n > 5);
bind (module SplitReturn) (fun n -> if n > 6 then "auto" else "");
()
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 84ec6ea9a83..8cda781691b 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -32,7 +32,7 @@ module CvalueDomain: Parameter_sig.Bool
module EqualityDomain: Parameter_sig.Bool
module GaugesDomain: Parameter_sig.Bool
module SymbolicLocsDomain: Parameter_sig.Bool
-module OctagonsDomain: Parameter_sig.Bool
+module OctagonDomain: Parameter_sig.Bool
module BitwiseOffsmDomain: Parameter_sig.Bool
module InoutDomain: Parameter_sig.Bool
module SignDomain: Parameter_sig.Bool
@@ -51,7 +51,7 @@ module EqualityCallFunction:
Parameter_sig.Map with type key = Cil_types.kernel_function
and type value = string
-module OctagonsCall: Parameter_sig.Bool
+module OctagonCall: Parameter_sig.Bool
module TracesUnrollLoop: Parameter_sig.Bool
module TracesUnifyLoop: Parameter_sig.Bool
diff --git a/tests/builtins/test_config_octagons b/tests/builtins/test_config_octagons
index 577aa8ef179..848a1c5fa41 100644
--- a/tests/builtins/test_config_octagons
+++ b/tests/builtins/test_config_octagons
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-octagons-domain
+MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-octagon-domain
MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_octagons b/tests/test_config_octagons
index 43c789be567..701bc8421e7 100644
--- a/tests/test_config_octagons
+++ b/tests/test_config_octagons
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-octagons-domain
+MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-octagon-domain
MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/value/octagons.c b/tests/value/octagons.c
index 34f6a719119..e30bb90ba1b 100644
--- a/tests/value/octagons.c
+++ b/tests/value/octagons.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +" -eva-octagons-domain -eva-octagons-through-calls -eva-msg-key=d-octagons,-d-cvalue"
+ STDOPT: +" -eva-octagon-domain -eva-octagon-through-calls -eva-msg-key=d-octagon,-d-cvalue"
*/
#include <__fc_builtin.h>
@@ -70,7 +70,7 @@ void arith () {
Frama_C_show_each_BOTTOM(a, b);
}
-/* Tests the join of the octagons domain. */
+/* Tests the join of the octagon domain. */
void join () {
int a, b, r;
int k = Frama_C_interval(-1, 4);
@@ -96,7 +96,7 @@ void join () {
Frama_C_show_each_join_negative(r);
}
-/* Tests the octagons domain within loops. */
+/* Tests the octagon domain within loops. */
void loop () {
int k = Frama_C_interval(-8, 8);
int a = Frama_C_interval(-1024, 1024);
@@ -117,7 +117,7 @@ void loop () {
Frama_C_show_each_precise(d3);
}
-/* Tests the soundness of the octagons domain in presence of pointers. */
+/* Tests the soundness of the octagon domain in presence of pointers. */
void pointers () {
int x, y, r;
int *px = &x, *pr = &r;
--
GitLab