From b935c31a8acfe7f2f823ebe1099d84b68d09652a Mon Sep 17 00:00:00 2001 From: thibautbenjamin <thibaut.benjamin@polytechnique.edu> Date: Tue, 20 Jul 2021 12:52:16 +0200 Subject: [PATCH] [e-acsl] headers --- src/plugins/e-acsl/headers/header_spec.txt | 6 +++++ .../src/analyses/preprocess_predicates.ml | 22 +++++++++++++++++++ .../src/analyses/preprocess_predicates.mli | 22 +++++++++++++++++++ .../e-acsl/src/analyses/preprocess_typing.ml | 22 +++++++++++++++++++ .../e-acsl/src/analyses/preprocess_typing.mli | 22 +++++++++++++++++++ .../e-acsl/src/code_generator/smart_term.ml | 22 +++++++++++++++++++ .../e-acsl/src/code_generator/smart_term.mli | 22 +++++++++++++++++++ 7 files changed, 138 insertions(+) diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt index ba5c6cbe99e..2f3f69b8c70 100644 --- a/src/plugins/e-acsl/headers/header_spec.txt +++ b/src/plugins/e-acsl/headers/header_spec.txt @@ -78,6 +78,10 @@ src/analyses/literal_strings.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/analyses/lscope.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/analyses/lscope.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/analyses/memory_tracking.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +src/analyses/preprocess_predicates.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +src/analyses/preprocess_predicates.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +src/analyses/preprocess_typing.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +src/analyses/preprocess_typing.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/analyses/memory_tracking.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/analyses/rte.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/analyses/rte.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL @@ -122,6 +126,8 @@ src/code_generator/smart_exp.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/code_generator/smart_exp.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/code_generator/smart_stmt.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/code_generator/smart_stmt.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +src/code_generator/smart_term.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +src/code_generator/smart_term.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/code_generator/temporal.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/code_generator/temporal.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/code_generator/translate.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL diff --git a/src/plugins/e-acsl/src/analyses/preprocess_predicates.ml b/src/plugins/e-acsl/src/analyses/preprocess_predicates.ml index 587b4fa4044..1239f07a741 100644 --- a/src/plugins/e-acsl/src/analyses/preprocess_predicates.ml +++ b/src/plugins/e-acsl/src/analyses/preprocess_predicates.ml @@ -1,3 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) +(* *) +(* Copyright (C) 2012-2020 *) +(* 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). *) +(* *) +(**************************************************************************) + open Cil_types open Lscope diff --git a/src/plugins/e-acsl/src/analyses/preprocess_predicates.mli b/src/plugins/e-acsl/src/analyses/preprocess_predicates.mli index c573a2a93c1..2a15a4e5823 100644 --- a/src/plugins/e-acsl/src/analyses/preprocess_predicates.mli +++ b/src/plugins/e-acsl/src/analyses/preprocess_predicates.mli @@ -1,3 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) +(* *) +(* Copyright (C) 2012-2020 *) +(* 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). *) +(* *) +(**************************************************************************) + open Cil_types val preprocess : file -> unit diff --git a/src/plugins/e-acsl/src/analyses/preprocess_typing.ml b/src/plugins/e-acsl/src/analyses/preprocess_typing.ml index 1a36141a135..3fbe5e5ac6b 100644 --- a/src/plugins/e-acsl/src/analyses/preprocess_typing.ml +++ b/src/plugins/e-acsl/src/analyses/preprocess_typing.ml @@ -1,3 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) +(* *) +(* Copyright (C) 2012-2020 *) +(* 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). *) +(* *) +(**************************************************************************) + open Cil_types let must_translate_ref : (Property.t -> bool) ref = diff --git a/src/plugins/e-acsl/src/analyses/preprocess_typing.mli b/src/plugins/e-acsl/src/analyses/preprocess_typing.mli index e59cd20b9be..61149052044 100644 --- a/src/plugins/e-acsl/src/analyses/preprocess_typing.mli +++ b/src/plugins/e-acsl/src/analyses/preprocess_typing.mli @@ -1,3 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) +(* *) +(* Copyright (C) 2012-2020 *) +(* 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). *) +(* *) +(**************************************************************************) + open Cil_types val must_translate_ref : (Property.t -> bool) ref diff --git a/src/plugins/e-acsl/src/code_generator/smart_term.ml b/src/plugins/e-acsl/src/code_generator/smart_term.ml index a9cf9bdb1a7..2290a3a203e 100644 --- a/src/plugins/e-acsl/src/code_generator/smart_term.ml +++ b/src/plugins/e-acsl/src/code_generator/smart_term.ml @@ -1,3 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) +(* *) +(* Copyright (C) 2012-2020 *) +(* 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). *) +(* *) +(**************************************************************************) + open Cil_types let is_pointer_type cty = diff --git a/src/plugins/e-acsl/src/code_generator/smart_term.mli b/src/plugins/e-acsl/src/code_generator/smart_term.mli index dccf9a0a78c..c2d03b6e88d 100644 --- a/src/plugins/e-acsl/src/code_generator/smart_term.mli +++ b/src/plugins/e-acsl/src/code_generator/smart_term.mli @@ -1,3 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of the Frama-C's E-ACSL plug-in. *) +(* *) +(* Copyright (C) 2012-2020 *) +(* 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). *) +(* *) +(**************************************************************************) + open Cil_types val is_pointer_type : typ -> bool -- GitLab