Commit 97267d51 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Apron domains registration.

parent 9772805f
......@@ -821,21 +821,12 @@ PLUGIN_TESTS_DIRS+=value/traces
# Files for the binding to Apron domains. Only available if Apron is available.
ifeq ($(HAS_APRON),yes)
PLUGIN_REQUIRES+= apron.octMPQ apron.boxMPQ apron.polkaMPQ apron.apron gmp
src/plugins/value/domains/apron/apron_domain.ml: \
src/plugins/value/domains/apron/apron_domain.ok.ml \
share/Makefile.config
$(CP_IF_DIFF) $< $@
$(CHMOD_RO) $@
APRON_CMO:= domains/apron/apron_domain
else
src/plugins/value/domains/apron/apron_domain.ml: \
src/plugins/value/domains/apron/apron_domain.ko.ml \
share/Makefile.config
$(CP_IF_DIFF) $< $@
$(CHMOD_RO) $@
endif
PLUGIN_GENERATED+= src/plugins/value/domains/apron/apron_domain.ml
APRON_CMO:=
PLUGIN_DISTRIB_EXTERNAL+= \
domains/apron/apron_domain.ok.ml domains/apron/apron_domain.ko.ml
domains/apron/apron_domain.ml domains/apron/apron_domain.mli
endif
# Files for the numerors domain. Only available is MPFR is available.
NUMERORS_FILES:= \
......@@ -890,7 +881,6 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
domains/traces_domain \
domains/simple_memory \
domains/gauges/gauges_domain \
domains/apron/apron_domain \
domains/hcexprs \
domains/equality/equality domains/equality/equality_domain \
domains/offsm_domain \
......@@ -918,7 +908,8 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
engine/partition engine/partitioning_parameters engine/trace_partitioning \
engine/iterator \
engine/initialization \
engine/compute_functions engine/analysis register
engine/compute_functions engine/analysis register \
$(APRON_CMO)
PLUGIN_CMI:= values/abstract_value values/abstract_location \
domains/abstract_domain domains/simpler_domains
PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen
......
(**************************************************************************)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
let ok = false
module type S = Abstract_domain.Leaf
with type value = Main_values.Interval.t
and type location = Precise_locs.precise_location
module U = struct
include Unit_domain.Make (Main_values.Interval) (Main_locations.PLoc)
let key = Structure.Key_Domain.create_key "dummy_apron"
end
module Octagon = U
module Box = U
module Polka_Loose = U
module Polka_Strict = U
module Polka_Equalities = U
(*
Local Variables:
compile-command: "make -C ../../../.."
End:
*)
......@@ -20,22 +20,14 @@
(* *)
(**************************************************************************)
#24 "src/plugins/value/domains/apron/apron_domain.ok.ml"
open Cil_types
open Eval
open Apron
let dkey = Value_parameters.register_category "d-apron"
let ok = true
let debug = false
module type S = Abstract_domain.Leaf
with type value = Main_values.Interval.t
and type location = Precise_locs.precise_location
let abort exclog =
let open Manager in
Value_parameters.fatal
......@@ -357,13 +349,13 @@ let ival_to_interval = function
(* Abstract Domain Functor *)
(* -------------------------------------------------------------------------- *)
module Make
(Man: sig
type t
val manager: t Manager.t
val name: string
end)
= struct
module type Input = sig
type t
val manager: t Manager.t
val name: string
end
module Make (Man : Input) = struct
type state = Man.t Abstract1.t
type value = Main_values.Interval.t
......@@ -753,11 +745,21 @@ end
(** Apron manager allocation changes the rounding mode. *)
let () = Floating_point.set_round_nearest_even ()
module Octagon = Domain_builder.Complete (Make (Apron_Octagon))
module Box = Domain_builder.Complete (Make (Apron_Box))
module Polka_Loose = Domain_builder.Complete (Make (Apron_Polka_Loose))
module Polka_Strict = Domain_builder.Complete (Make (Apron_Polka_Strict))
module Polka_Equalities = Domain_builder.Complete (Make (Apron_Polka_Equalities))
let make name enable (module Man: Input) =
let module Domain = Domain_builder.Complete (Make (Man)) in
let open Abstractions in
register ~enable { name;
values = Single (module Main_values.Interval);
domain = Domain (module Domain); }
let () =
let open Value_parameters in
make "apron octagons" ApronOctagon.get (module Apron_Octagon);
make "apron box" ApronBox.get (module Apron_Box);
make "polka loose" PolkaLoose.get (module Apron_Polka_Loose);
make "polka strict" PolkaStrict.get (module Apron_Polka_Strict);
make "polka equalities" PolkaEqualities.get (module Apron_Polka_Equalities);
register_apron ()
(*
......
......@@ -24,33 +24,6 @@
the APRON library: http://apron.cri.ensmp.fr/library
For now, this binding only processes scalar integer variables. *)
(** Are apron domains available? *)
val ok : bool
(** Signature of an Apron domain in Eva. *)
module type S = Abstract_domain.Leaf
with type value = Main_values.Interval.t
and type location = Precise_locs.precise_location
(** Apron domains available for Eva. *)
(** Octagons abstract domain. *)
module Octagon : S
(** Intervals abstract domain. *)
module Box : S
(** Loose polyhedra of the NewPolka library.
Cannot have strict inequality constraints. Algorithmically more efficient. *)
module Polka_Loose : S
(** Strict polyhedra of the NewPolka library. *)
module Polka_Strict : S
(** Linear equalities. *)
module Polka_Equalities : S
(*
Local Variables:
compile-command: "make -C ../../../.."
......
......@@ -77,6 +77,8 @@ let dkey_incompatible_states = register_category "incompatible-states"
let dkey_iterator = register_category "iterator"
let dkey_callbacks = register_category "callbacks"
let dkey_widening = register_category "widening"
let dkey_experimental = register_category "experimental-ok"
let () =
let activate dkey = add_debug_keys dkey in
......@@ -184,12 +186,23 @@ module NumerorsDomain = Domain_Parameter
let apron_help = "Experimental binding of the numerical domains provided \
by the APRON library: http://apron.cri.ensmp.fr/library \n"
let apron_available = ref false
let register_apron () = apron_available := true
let apron_hook _ _ =
if not !apron_available
then
abort "an Apron domain is requested but the apron binding is not available."
else if not (is_debug_key_enabled dkey_experimental) then
warning "The Apron domains binding is experimental.";
module ApronOctagon = Domain_Parameter
(struct
let option_name = "-eva-apron-oct"
let help = apron_help ^ "Use the octagon domain of apron."
let default = false
end)
let () = ApronOctagon.add_set_hook apron_hook
module ApronBox = Domain_Parameter
(struct
......@@ -197,6 +210,7 @@ module ApronBox = Domain_Parameter
let help = apron_help ^ "Use the box domain of apron."
let default = false
end)
let () = ApronBox.add_set_hook apron_hook
module PolkaLoose = Domain_Parameter
(struct
......@@ -204,6 +218,7 @@ module PolkaLoose = Domain_Parameter
let help = apron_help ^ "Use the loose polyhedra domain of apron."
let default = false
end)
let () = PolkaLoose.add_set_hook apron_hook
module PolkaStrict = Domain_Parameter
(struct
......@@ -211,6 +226,7 @@ module PolkaStrict = Domain_Parameter
let help = apron_help ^ "Use the strict polyhedra domain of apron."
let default = false
end)
let () = PolkaStrict.add_set_hook apron_hook
module PolkaEqualities = Domain_Parameter
(struct
......@@ -218,6 +234,7 @@ module PolkaEqualities = Domain_Parameter
let help = apron_help ^ "Use the linear equalities domain of apron."
let default = false
end)
let () = PolkaEqualities.add_set_hook apron_hook
module InoutDomain = Domain_Parameter
(struct
......
......@@ -234,6 +234,8 @@ val dkey_callbacks : category
val dkey_widening : category
(** Notifies that the binding to Apron domains is available. *)
val register_apron: unit -> unit
(*
Local Variables:
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment