From 437794a8e2b74e523be46311e73515eafd3ee9ce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Mon, 4 Dec 2017 17:58:04 +0100 Subject: [PATCH] [Eva] Headers for the errors value and domain. --- headers/header_spec.txt | 4 ++++ src/plugins/value/values/errors_value.ml | 22 ++++++++++++++++++++++ src/plugins/value/values/errors_value.mli | 22 ++++++++++++++++++++++ 3 files changed, 48 insertions(+) diff --git a/headers/header_spec.txt b/headers/header_spec.txt index c770275d9ca..881dcf372c6 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -1133,6 +1133,8 @@ src/plugins/value/domains/powerset.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/value/domains/powerset.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/value/domains/sign_domain.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/value/domains/sign_domain.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/value/domains/errors_domain.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/value/domains/errors_domain.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/value/domains/simple_memory.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/value/domains/simple_memory.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/value/domains/symbolic_locs.ml: CEA_LGPL_OR_PROPRIETARY @@ -1247,6 +1249,8 @@ src/plugins/value/values/offsm_value.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/value/values/offsm_value.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/value/values/sign_value.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/value/values/sign_value.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/value/values/errors_value.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/value/values/errors_value.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/value/values/value_product.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/value/values/value_product.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/value_types/README.md: .ignore diff --git a/src/plugins/value/values/errors_value.ml b/src/plugins/value/values/errors_value.ml index 0cb7d4c9768..2da8236496a 100644 --- a/src/plugins/value/values/errors_value.ml +++ b/src/plugins/value/values/errors_value.ml @@ -1,3 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2017 *) +(* 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 Eval open Abstract_interp diff --git a/src/plugins/value/values/errors_value.mli b/src/plugins/value/values/errors_value.mli index 5baea128d4a..fe27811f6f7 100644 --- a/src/plugins/value/values/errors_value.mli +++ b/src/plugins/value/values/errors_value.mli @@ -1,3 +1,25 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2017 *) +(* 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). *) +(* *) +(**************************************************************************) + include Abstract_value.Internal val pretty_debug : t Pretty_utils.formatter -- GitLab