From f4e23690d20d28b611e2ba9675b81a3d337cccda Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 18 Nov 2020 19:43:24 +0100
Subject: [PATCH] [Aorai] Use Eva as an optional dependency
---
headers/header_spec.txt | 3 +++
src/plugins/aorai/.gitignore | 1 +
src/plugins/aorai/Makefile.in | 26 ++++++++++++++++++-
.../aorai/aorai_eva_analysis.disabled.ml | 26 +++++++++++++++++++
.../aorai/aorai_eva_analysis.enabled.ml | 26 +++++++++++++++++++
src/plugins/aorai/aorai_eva_analysis.mli | 26 +++++++++++++++++++
src/plugins/aorai/aorai_register.ml | 1 +
7 files changed, 108 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/aorai/aorai_eva_analysis.disabled.ml
create mode 100644 src/plugins/aorai/aorai_eva_analysis.enabled.ml
create mode 100644 src/plugins/aorai/aorai_eva_analysis.mli
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 69a036f5610..06b913c3cc7 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -718,6 +718,9 @@ src/plugins/aorai/VERSIONS.txt: .ignore
src/plugins/aorai/YA.README: .ignore
src/plugins/aorai/aorai_dataflow.ml: AORAI_LGPL
src/plugins/aorai/aorai_dataflow.mli: AORAI_LGPL
+src/plugins/aorai/aorai_eva_analysis.disabled.ml: AORAI_LGPL
+src/plugins/aorai/aorai_eva_analysis.enabled.ml: AORAI_LGPL
+src/plugins/aorai/aorai_eva_analysis.mli: AORAI_LGPL
src/plugins/aorai/aorai_graph.ml: AORAI_LGPL
src/plugins/aorai/aorai_graph.mli: AORAI_LGPL
src/plugins/aorai/aorai_metavariables.ml: AORAI_LGPL
diff --git a/src/plugins/aorai/.gitignore b/src/plugins/aorai/.gitignore
index dbc3d247b66..6e2440c7d50 100644
--- a/src/plugins/aorai/.gitignore
+++ b/src/plugins/aorai/.gitignore
@@ -1,4 +1,5 @@
/tests/ptests_config
+/aorai_eva_analysis.ml
/Makefile
/ltllexer.ml
/ltlparser.ml
diff --git a/src/plugins/aorai/Makefile.in b/src/plugins/aorai/Makefile.in
index c39a616ce7e..dfb9ab78cc8 100644
--- a/src/plugins/aorai/Makefile.in
+++ b/src/plugins/aorai/Makefile.in
@@ -41,6 +41,7 @@ PLUGIN_DIR ?=.
PLUGIN_ENABLE:=@ENABLE_AORAI@
PLUGIN_NAME:=Aorai
PLUGIN_GENERATED:= $(addprefix ${PLUGIN_DIR}/, \
+ aorai_eva_analysis.ml \
promelalexer_withexps.ml promelaparser_withexps.ml \
promelaparser_withexps.mli \
promelalexer.ml promelaparser.ml promelaparser.mli \
@@ -67,13 +68,36 @@ PLUGIN_CMO:= bool3 \
promelalexer_withexps \
aorai_dataflow \
aorai_visitors \
+ aorai_eva_analysis \
aorai_register
PLUGIN_CMI:= ltlast promelaast
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
-PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
+PLUGIN_DISTRIB_EXTERNAL:= \
+ aorai_eva_analysis.enabled.ml aorai_eva_analysis.disabled.ml \
+ Makefile.in configure.ac configure
PLUGIN_HAS_EXT_DOC:=no # [JS 2010/07/28] was 'yes'
# but prevent 'make src-distrib to work
+PLUGIN_DEPENDENCIES:=
+
+# Dynamic dependencies
+
+$(PLUGIN_DIR)/aorai_eva_analysis.ml:
+ $(PRINT_MAKING) $@
+ $(CP) $< $@
+ $(CHMOD_RO) $@
+
+ifneq "$(ENABLE_EVA)" "no"
+PLUGIN_DEPENDENCIES+= Eva
+$(PLUGIN_DIR)/aorai_eva_analysis.ml: $(PLUGIN_DIR)/aorai_eva_analysis.enabled.ml
+else
+$(PLUGIN_DIR)/aorai_eva_analysis.ml: $(PLUGIN_DIR)/aorai_eva_analysis.disabled.ml
+endif
+
+$(PLUGIN_DIR)/aorai_eva_analysis.ml: $(PLUGIN_DIR)/Makefile share/Makefile.config
+
+
+# Tests
# aorai_ya can always be run
PLUGIN_TESTS_DIRS:=ya
diff --git a/src/plugins/aorai/aorai_eva_analysis.disabled.ml b/src/plugins/aorai/aorai_eva_analysis.disabled.ml
new file mode 100644
index 00000000000..b17dd3dae1b
--- /dev/null
+++ b/src/plugins/aorai/aorai_eva_analysis.disabled.ml
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Aorai plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* INSA (Institut National des Sciences Appliquees) *)
+(* *)
+(* 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 setup () = ()
diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
new file mode 100644
index 00000000000..b17dd3dae1b
--- /dev/null
+++ b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Aorai plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* INSA (Institut National des Sciences Appliquees) *)
+(* *)
+(* 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 setup () = ()
diff --git a/src/plugins/aorai/aorai_eva_analysis.mli b/src/plugins/aorai/aorai_eva_analysis.mli
new file mode 100644
index 00000000000..8f6790f45f5
--- /dev/null
+++ b/src/plugins/aorai/aorai_eva_analysis.mli
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Aorai plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* INSA (Institut National des Sciences Appliquees) *)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val setup : unit -> unit
diff --git a/src/plugins/aorai/aorai_register.ml b/src/plugins/aorai/aorai_register.ml
index 3c9e51b03d5..6bd2ed39407 100644
--- a/src/plugins/aorai/aorai_register.ml
+++ b/src/plugins/aorai/aorai_register.ml
@@ -356,6 +356,7 @@ let work () =
if Aorai_option.GenerateAnnotations.get () then
Aorai_visitors.add_pre_post_from_buch file
(Aorai_option.advance_abstract_interpretation ());
+ Aorai_eva_analysis.setup ();
printverb "Annotation of Cil : done\n";
end
end
--
GitLab