diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 69a036f5610cc986d402c06130367d7c7dd673b4..06b913c3cc70a0afae8ace3b73756565deca027c 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 dbc3d247b6627099a25ed2b34608c057d6120bfe..6e2440c7d5053e68723ce0ec0a462d751551dda1 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 c39a616ce7e5ea1bb53d8bbd826cdc308701d539..dfb9ab78cc822aa72b8267e6de9a7933dec39972 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 0000000000000000000000000000000000000000..b17dd3dae1bb60c238aeee9060a17c1373bc52dd
--- /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 0000000000000000000000000000000000000000..b17dd3dae1bb60c238aeee9060a17c1373bc52dd
--- /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 0000000000000000000000000000000000000000..8f6790f45f59923cbd32dbb34e38365ccaf82bf3
--- /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 3c9e51b03d5b850a60df4c04df56cbcb073e5b1e..6bd2ed394074ddd199d9511c3e991de7518dc4fd 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