diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt index ba5c6cbe99e0249a9262f797c3c74c954d047600..2f3f69b8c70d095f926e8cc9589d0f7cf310b3bd 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 587b4fa404488347bfea4a3e031907b4d1e2ef01..1239f07a7413d534020f48b48e84bea673d6f7d1 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 c573a2a93c12275999197ae56f740e8f12cde247..2a15a4e582347df4cc465f831f104529480c4645 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 1a36141a135b5d332c20e0945815aa952a1d5787..3fbe5e5ac6bb6cac2a9846deeb6c1f36134bff37 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 e59cd20b9be1454e407188415f849cd60fc3b3cf..61149052044c5e9a0dc3dfbf6fa21c29c9667cae 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 a9cf9bdb1a75aaac1c4fd7f73776aaac20a98c3b..2290a3a203e6d0538d1621a14e2e6311a89d489c 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 dccf9a0a78c268c3899454878c0412970f11a37b..c2d03b6e88d61deca26be752360b8a75d03dbee5 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