From f005ac01c6e8355ac7728c853f290a1476c5a12d Mon Sep 17 00:00:00 2001 From: Julien Signoles <julien.signoles@cea.fr> Date: Thu, 19 Sep 2019 20:08:42 +0200 Subject: [PATCH] [archi] add injector --- src/plugins/e-acsl/Makefile.in | 3 ++- .../e-acsl/src/code_generator/injector.ml | 27 +++++++++++++++++++ .../e-acsl/src/code_generator/injector.mli | 27 +++++++++++++++++++ 3 files changed, 56 insertions(+), 1 deletion(-) create mode 100644 src/plugins/e-acsl/src/code_generator/injector.ml create mode 100644 src/plugins/e-acsl/src/code_generator/injector.mli diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index c09bfba0016..ba6c3dc0200 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -76,7 +76,8 @@ SRC_CODE_GENERATOR:= \ logic_functions \ translate \ temporal \ - visit + visit \ + injector SRC_CODE_GENERATOR:=$(addprefix src/code_generator/, $(SRC_CODE_GENERATOR)) ######################### diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml new file mode 100644 index 00000000000..6cc68db52cf --- /dev/null +++ b/src/plugins/e-acsl/src/code_generator/injector.ml @@ -0,0 +1,27 @@ +(**************************************************************************) +(* *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) +(* *) +(* Copyright (C) 2012-2018 *) +(* 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). *) +(* *) +(**************************************************************************) + +(* +Local Variables: +compile-command: "make -C ../.." +End: +*) diff --git a/src/plugins/e-acsl/src/code_generator/injector.mli b/src/plugins/e-acsl/src/code_generator/injector.mli new file mode 100644 index 00000000000..6cc68db52cf --- /dev/null +++ b/src/plugins/e-acsl/src/code_generator/injector.mli @@ -0,0 +1,27 @@ +(**************************************************************************) +(* *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) +(* *) +(* Copyright (C) 2012-2018 *) +(* 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). *) +(* *) +(**************************************************************************) + +(* +Local Variables: +compile-command: "make -C ../.." +End: +*) -- GitLab