Skip to content
Snippets Groups Projects
Commit f4e23690 authored by Valentin Perrelle's avatar Valentin Perrelle Committed by Virgile Prevosto
Browse files

[Aorai] Use Eva as an optional dependency

parent e58f880c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
headers/header_spec.txt
+ 3
− 0
View file @ f4e23690
...@@ -718,6 +718,9 @@ src/plugins/aorai/VERSIONS.txt: .ignore ...@@ -718,6 +718,9 @@ src/plugins/aorai/VERSIONS.txt: .ignore
src/plugins/aorai/YA.README: .ignore src/plugins/aorai/YA.README: .ignore
src/plugins/aorai/aorai_dataflow.ml: AORAI_LGPL src/plugins/aorai/aorai_dataflow.ml: AORAI_LGPL
src/plugins/aorai/aorai_dataflow.mli: 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.ml: AORAI_LGPL
src/plugins/aorai/aorai_graph.mli: AORAI_LGPL src/plugins/aorai/aorai_graph.mli: AORAI_LGPL
src/plugins/aorai/aorai_metavariables.ml: AORAI_LGPL src/plugins/aorai/aorai_metavariables.ml: AORAI_LGPL
......
src/plugins/aorai/.gitignore
+ 1
− 0
View file @ f4e23690
/tests/ptests_config /tests/ptests_config
/aorai_eva_analysis.ml
/Makefile /Makefile
/ltllexer.ml /ltllexer.ml
/ltlparser.ml /ltlparser.ml
......
src/plugins/aorai/Makefile.in
+ 25
− 1
View file @ f4e23690
...@@ -41,6 +41,7 @@ PLUGIN_DIR ?=. ...@@ -41,6 +41,7 @@ PLUGIN_DIR ?=.
PLUGIN_ENABLE:=@ENABLE_AORAI@ PLUGIN_ENABLE:=@ENABLE_AORAI@
PLUGIN_NAME:=Aorai PLUGIN_NAME:=Aorai
PLUGIN_GENERATED:= $(addprefix ${PLUGIN_DIR}/, \ PLUGIN_GENERATED:= $(addprefix ${PLUGIN_DIR}/, \
aorai_eva_analysis.ml \
promelalexer_withexps.ml promelaparser_withexps.ml \ promelalexer_withexps.ml promelaparser_withexps.ml \
promelaparser_withexps.mli \ promelaparser_withexps.mli \
promelalexer.ml promelaparser.ml promelaparser.mli \ promelalexer.ml promelaparser.ml promelaparser.mli \
...@@ -67,13 +68,36 @@ PLUGIN_CMO:= bool3 \ ...@@ -67,13 +68,36 @@ PLUGIN_CMO:= bool3 \
promelalexer_withexps \ promelalexer_withexps \
aorai_dataflow \ aorai_dataflow \
aorai_visitors \ aorai_visitors \
aorai_eva_analysis \
aorai_register aorai_register
PLUGIN_CMI:= ltlast promelaast PLUGIN_CMI:= ltlast promelaast
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE) 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' PLUGIN_HAS_EXT_DOC:=no # [JS 2010/07/28] was 'yes'
# but prevent 'make src-distrib to work # 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 # aorai_ya can always be run
PLUGIN_TESTS_DIRS:=ya PLUGIN_TESTS_DIRS:=ya
......
src/plugins/aorai/aorai_eva_analysis.disabled.ml 0 → 100644
+ 26
− 0
View file @ f4e23690
(**************************************************************************)
(* *)
(* 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 () = ()
src/plugins/aorai/aorai_eva_analysis.enabled.ml 0 → 100644
+ 26
− 0
View file @ f4e23690
(**************************************************************************)
(* *)
(* 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 () = ()
src/plugins/aorai/aorai_eva_analysis.mli 0 → 100644
+ 26
− 0
View file @ f4e23690
(**************************************************************************)
(* *)
(* 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
src/plugins/aorai/aorai_register.ml
+ 1
− 0
View file @ f4e23690
...@@ -356,6 +356,7 @@ let work () = ...@@ -356,6 +356,7 @@ let work () =
if Aorai_option.GenerateAnnotations.get () then if Aorai_option.GenerateAnnotations.get () then
Aorai_visitors.add_pre_post_from_buch file Aorai_visitors.add_pre_post_from_buch file
(Aorai_option.advance_abstract_interpretation ()); (Aorai_option.advance_abstract_interpretation ());
Aorai_eva_analysis.setup ();
printverb "Annotation of Cil : done\n"; printverb "Annotation of Cil : done\n";
end end
end end
......
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