[Eva] use singular form for octagon domain

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}

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

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)

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

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 "");
   ()
 

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

tests/builtins/test_config_octagons

-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

tests/test_config_octagons

-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

tests/value/octagons.c

 /* 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;