[Eva] New octagons domain.

Makefile

@@ -875,6 +875,7 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
 	domains/printer_domain \
 	domains/traces_domain \
 	domains/simple_memory \
+	domains/octagons \
 	domains/gauges/gauges_domain \
 	domains/hcexprs \
 	domains/equality/equality domains/equality/equality_domain \

headers/header_spec.txt

@@ -1189,6 +1189,8 @@ src/plugins/value/domains/hcexprs.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/hcexprs.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/inout_domain.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/inout_domain.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/octagons.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/octagons.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/offsm_domain.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/offsm_domain.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/value/domains/powerset.ml: CEA_LGPL_OR_PROPRIETARY

src/plugins/value/domains/octagons.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2019                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+include Abstract_domain.Leaf
+  with type value = Cvalue.V.t
+   and type location = Precise_locs.precise_location

src/plugins/value/value_parameters.ml

@@ -167,6 +167,13 @@ module SymbolicLocsDomain = Domain_Parameter
       let default = false
     end)
 
+module OctagonsDomain = Domain_Parameter
+    (struct
+      let option_name = "-eva-octagons-domain"
+      let help = "Use the octagons domain of Eva."
+      let default = false
+    end)
+
 module BitwiseOffsmDomain = Domain_Parameter
     (struct
       let option_name = "-eva-bitwise-domain"

src/plugins/value/value_parameters.mli

@@ -32,6 +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 BitwiseOffsmDomain: Parameter_sig.Bool
 module InoutDomain: Parameter_sig.Bool
 module SignDomain: Parameter_sig.Bool