diff --git a/headers/header_spec.txt b/headers/header_spec.txt index c770275d9ca9adcf49800cea23e13be34749ad6f..881dcf372c66099f5f9b394b2a8e9928b263fe71 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 0cb7d4c9768fd0a71d71bea659cb2d23949c8132..2da8236496a1710eda40bee58be2631aaa8cc59a 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 5baea128d4a7616b48f63e58311e384663393e83..fe27811f6f74b7eeb7b929da05c7026a4f796c1b 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