diff --git a/Makefile b/Makefile
index 233831ab22d1783d9e4ca97a4b44d18ecb59ef55..0d2195c2245f418d6e68c5cad0e75826b4689c80 100644
--- a/Makefile
+++ b/Makefile
@@ -751,7 +751,8 @@ PLUGIN_ENABLE:=$(ENABLE_EVA)
PLUGIN_NAME:=Eva
PLUGIN_DIR:=src/plugins/value
PLUGIN_EXTRA_DIRS:=engine values domains domains/cvalue domains/apron \
- domains/gauges domains/equality legacy slevel utils gui_files
+ domains/gauges domains/equality legacy slevel utils gui_files \
+ domains/numerors values/numerors
# General rules for ordering files within PLUGIN_CMO:
# - try to keep the legacy Value before Eva
PLUGIN_CMO:= slevel/split_strategy value_parameters \
@@ -767,7 +768,9 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
values/cvalue_forward values/cvalue_backward \
values/main_values values/main_locations \
values/offsm_value values/sign_value \
- values/errors_value \
+ values/numerors/numerors_utils \
+ values/numerors/numerors_float \
+ values/numerors/numerors_value \
legacy/eval_op legacy/function_args \
domains/domain_store domains/domain_builder \
domains/domain_product domains/domain_lift domains/unit_domain \
@@ -780,7 +783,7 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
domains/offsm_domain \
domains/symbolic_locs \
domains/sign_domain \
- domains/errors_domain \
+ domains/numerors/numerors_domain \
domains/cvalue/warn domains/cvalue/locals_scoping \
domains/cvalue/cvalue_offsetmap \
utils/value_results \
@@ -826,19 +829,20 @@ PLUGIN_DISTRIB_EXTERNAL:=domains/apron/apron_domain.ok.ml domains/apron/apron_do
ifeq ($(HAS_MPFR),yes)
PLUGIN_REQUIRES:= gmp
-src/plugins/value/values/errors_value.ml: \
- src/plugins/value/values/errors_value.ok.ml share/Makefile.config
+src/plugins/value/values/numerors/numerors_value.ml: \
+ src/plugins/value/values/numerors/numerors_value.ok.ml share/Makefile.config
$(CP_IF_DIFF) $< $@
$(CHMOD_RO) $@
else
PLUGIN_REQUIRES:=
-src/plugins/value/values/errors_value.ml: \
- src/plugins/value/values/errors_value.ko.ml share/Makefile.config
+src/plugins/value/values/numerors/numerors_value.ml: \
+ src/plugins/value/values/numerors/numerors_value.ko.ml share/Makefile.config
$(CP_IF_DIFF) $< $@
$(CHMOD_RO) $@
endif
-GENERATED += src/plugins/value/values.errors_value.ml
-PLUGIN_DISTRIB_EXTERNAL:=values/errors_value.ok.ml values/errors_value.ko.ml
+GENERATED += src/plugins/value/values/numerors/numerors_value.ml
+PLUGIN_DISTRIB_EXTERNAL:= \
+ values/numerors/numerors_value.ok.ml values/numerors/numerors_value.ko.ml
# These files are used by the GUI, but do not depend on Lablgtk
VALUE_GUI_AUX:=gui_files/gui_types gui_files/gui_eval \
diff --git a/configure.in b/configure.in
index b08b5ff6c69162827a8205c11e82722bc79a02bd..5de5785d43a7e223fb98f99608455e33356ee611 100644
--- a/configure.in
+++ b/configure.in
@@ -378,7 +378,7 @@ if test -f "$MPFR_PATH/gmp.$DYN_SUFFIX"; then
AC_MSG_RESULT(found)
else
HAS_MPFR="no";
- AC_MSG_RESULT(not found. The numeric error domain won't be available in Eva)
+ AC_MSG_RESULT(not found. The numerors domain won't be available in Eva)
fi;
# landmarks (profiling tool, for developers)
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 881dcf372c66099f5f9b394b2a8e9928b263fe71..9be6868f252bfbf9aacb7eceafc0d2b03c88c309 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1133,8 +1133,8 @@ src/plugins/value/domains/powerset.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/powerset.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/sign_domain.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/sign_domain.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/errors_domain.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/domains/errors_domain.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/numerors/numerors_domain.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/numerors/numerors_domain.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/simple_memory.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/simple_memory.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/symbolic_locs.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1249,8 +1249,8 @@ src/plugins/value/values/offsm_value.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/values/offsm_value.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/values/sign_value.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/values/sign_value.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/errors_value.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/values/errors_value.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/values/numerors/numerors_value.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/values/numerors/numerors_value.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/values/value_product.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/values/value_product.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value_types/README.md: .ignore
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ml b/src/plugins/value/domains/numerors/numerors_domain.ml
index 875f71f2bd46caa4308b7b56a1145d414db6d9dd..a2d1e10f8208986c47f43632dc43dd9b8f7f4f60 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ml
@@ -22,8 +22,8 @@
open Cil_types
-module Errors_Value = struct
- include Errors_value
+module Numerors_Value = struct
+ include Numerors_value
(* In this domain, we only track floating-point variables. *)
let track_variable vi = Cil.isFloatingType vi.vtype
@@ -32,4 +32,5 @@ module Errors_Value = struct
let widen = join
end
-include Simple_memory.Make_Domain (struct let name = "errors" end) (Errors_Value)
+include Simple_memory.Make_Domain (struct let name = "errors" end)
+ (Numerors_Value)
diff --git a/src/plugins/value/domains/numerors/numerors_domain.mli b/src/plugins/value/domains/numerors/numerors_domain.mli
index 72ee2b909fdf4a76f22b40a49a90d6b42ba118ca..f82a82b8dfc840093725c5bc6c36c12aea433abc 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.mli
+++ b/src/plugins/value/domains/numerors/numerors_domain.mli
@@ -22,5 +22,5 @@
(** Abstraction of the sign of integer variables. *)
-include Abstract_domain.Internal with type value = Errors_value.t
+include Abstract_domain.Internal with type value = Numerors_value.t
and type location = Precise_locs.precise_location
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 343e4a9baf92d7aabbad92c83a2d1a61ffa72f59..953ef0d93c7e08c29ae6716fa5185523dda66671 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -146,7 +146,7 @@ let build_value config =
let value =
if config.errors
then
- let module V = Value_product.Make ((val value)) (Errors_value) in
+ let module V = Value_product.Make ((val value)) (Numerors_value) in
(module V: Abstract_value.Internal)
else value
in
@@ -395,11 +395,11 @@ let add_signs abstract =
let add_errors abstract =
let module Abstract = (val abstract : Abstract) in
let module K = struct
- type v = Errors_value.t
- let key = Errors_value.error_key
+ type v = Numerors_value.t
+ let key = Numerors_value.error_key
end in
let module Conv = Convert (Abstract.Val) (K) in
- let module Errors = Domain_lift.Make (Errors_domain) (Conv) in
+ let module Errors = Domain_lift.Make (Numerors_domain) (Conv) in
let module Dom = Domain_product.Make (Abstract.Val) (Abstract.Dom) (Errors) in
(module struct
module Val = Abstract.Val
@@ -537,10 +537,10 @@ module Reduce (Value : Abstract_value.External) = struct
| _, _ -> fun x -> x
let reduce_error =
- match Value.get Errors_value.error_key, Value.get Main_values.cvalue_key with
+ match Value.get Numerors_value.error_key, Value.get Main_values.cvalue_key with
| Some get_error, Some get_cvalue ->
begin
- let set_error = Value.set Errors_value.error_key in
+ let set_error = Value.set Numerors_value.error_key in
fun t ->
let cvalue = get_cvalue t in
try
@@ -549,7 +549,7 @@ module Reduce (Value : Abstract_value.External) = struct
| Ival.Float fval ->
begin
let error = get_error t in
- let error = Errors_value.reduce fval error in
+ let error = Numerors_value.reduce fval error in
match error with
| `Value error -> set_error error t
| `Bottom -> t (* TODO: we should be able to reduce to bottom. *)