diff --git a/src/kernel_externals/value_types/README.md b/src/kernel_externals/value_types/README.md deleted file mode 100644 index 8aa4a28e5573a4ea1094fdb56c6819b9ff9fb9c2..0000000000000000000000000000000000000000 --- a/src/kernel_externals/value_types/README.md +++ /dev/null @@ -1,2 +0,0 @@ -This directory contains lattices representing the C memory model of Value, -and some of its derived plugins (From, Inout). diff --git a/src/kernel_services/abstract_interp/README.md b/src/kernel_services/abstract_interp/README.md index 22922767c6b73dbf5ae4a365d45c18dee11bf0ef..ce5ff5660c34ff67e31618b1a33d46fbb5cd452d 100644 --- a/src/kernel_services/abstract_interp/README.md +++ b/src/kernel_services/abstract_interp/README.md @@ -1,3 +1,4 @@ -This directory contains generic lattices for abstract interpretation. +This directory contains generic lattices for abstract interpretation +and the C memory model of Eva. -Nowadays it is mainly used by the Value plug-in and its derived plug-ins. +It is mainly used by Eva and its derived plug-ins (From, Inout). diff --git a/src/kernel_externals/value_types/cilE.ml b/src/kernel_services/abstract_interp/cilE.ml similarity index 100% rename from src/kernel_externals/value_types/cilE.ml rename to src/kernel_services/abstract_interp/cilE.ml diff --git a/src/kernel_externals/value_types/cilE.mli b/src/kernel_services/abstract_interp/cilE.mli similarity index 100% rename from src/kernel_externals/value_types/cilE.mli rename to src/kernel_services/abstract_interp/cilE.mli diff --git a/src/kernel_externals/value_types/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml similarity index 100% rename from src/kernel_externals/value_types/cvalue.ml rename to src/kernel_services/abstract_interp/cvalue.ml diff --git a/src/kernel_externals/value_types/cvalue.mli b/src/kernel_services/abstract_interp/cvalue.mli similarity index 100% rename from src/kernel_externals/value_types/cvalue.mli rename to src/kernel_services/abstract_interp/cvalue.mli diff --git a/src/kernel_externals/value_types/function_Froms.ml b/src/kernel_services/abstract_interp/function_Froms.ml similarity index 100% rename from src/kernel_externals/value_types/function_Froms.ml rename to src/kernel_services/abstract_interp/function_Froms.ml diff --git a/src/kernel_externals/value_types/function_Froms.mli b/src/kernel_services/abstract_interp/function_Froms.mli similarity index 100% rename from src/kernel_externals/value_types/function_Froms.mli rename to src/kernel_services/abstract_interp/function_Froms.mli diff --git a/src/kernel_externals/value_types/inout_type.ml b/src/kernel_services/abstract_interp/inout_type.ml similarity index 100% rename from src/kernel_externals/value_types/inout_type.ml rename to src/kernel_services/abstract_interp/inout_type.ml diff --git a/src/kernel_externals/value_types/inout_type.mli b/src/kernel_services/abstract_interp/inout_type.mli similarity index 100% rename from src/kernel_externals/value_types/inout_type.mli rename to src/kernel_services/abstract_interp/inout_type.mli diff --git a/src/kernel_externals/value_types/precise_locs.ml b/src/kernel_services/abstract_interp/precise_locs.ml similarity index 100% rename from src/kernel_externals/value_types/precise_locs.ml rename to src/kernel_services/abstract_interp/precise_locs.ml diff --git a/src/kernel_externals/value_types/precise_locs.mli b/src/kernel_services/abstract_interp/precise_locs.mli similarity index 100% rename from src/kernel_externals/value_types/precise_locs.mli rename to src/kernel_services/abstract_interp/precise_locs.mli diff --git a/src/kernel_externals/value_types/value_types.ml b/src/kernel_services/abstract_interp/value_types.ml similarity index 100% rename from src/kernel_externals/value_types/value_types.ml rename to src/kernel_services/abstract_interp/value_types.ml diff --git a/src/kernel_externals/value_types/value_types.mli b/src/kernel_services/abstract_interp/value_types.mli similarity index 100% rename from src/kernel_externals/value_types/value_types.mli rename to src/kernel_services/abstract_interp/value_types.mli diff --git a/src/kernel_externals/value_types/widen_type.ml b/src/kernel_services/abstract_interp/widen_type.ml similarity index 100% rename from src/kernel_externals/value_types/widen_type.ml rename to src/kernel_services/abstract_interp/widen_type.ml diff --git a/src/kernel_externals/value_types/widen_type.mli b/src/kernel_services/abstract_interp/widen_type.mli similarity index 100% rename from src/kernel_externals/value_types/widen_type.mli rename to src/kernel_services/abstract_interp/widen_type.mli