From d476fc9c48a3eababa9e68e5c9abdcc390fc2c24 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Tue, 30 Apr 2024 17:58:26 +0200 Subject: [PATCH] [headers] fix missing blank line at end of header --- src/kernel_internals/parsing/clexer.mli | 1 + src/kernel_internals/parsing/clexer.mll | 1 + src/kernel_internals/parsing/cparser.mly | 1 + src/kernel_internals/parsing/errorloc.ml | 1 + src/kernel_internals/parsing/errorloc.mli | 1 + src/kernel_internals/parsing/lexerhack.ml | 1 + src/kernel_internals/parsing/lexerhack.mli | 1 + src/kernel_internals/typing/alpha.ml | 1 + src/kernel_internals/typing/alpha.mli | 1 + src/kernel_internals/typing/cabs2cil.ml | 1 + src/kernel_internals/typing/cabs2cil.mli | 1 + src/kernel_internals/typing/cfg.ml | 1 + src/kernel_internals/typing/cfg.mli | 1 + src/kernel_internals/typing/frontc.ml | 1 + src/kernel_internals/typing/frontc.mli | 1 + src/kernel_internals/typing/mergecil.ml | 1 + src/kernel_internals/typing/mergecil.mli | 1 + src/kernel_internals/typing/oneret.ml | 1 + src/kernel_internals/typing/oneret.mli | 1 + src/kernel_internals/typing/rmtmps.ml | 1 + src/kernel_internals/typing/rmtmps.mli | 1 + src/kernel_services/analysis/dataflows.ml | 1 + src/kernel_services/analysis/dataflows.mli | 1 + src/kernel_services/ast_data/cil_types.ml | 1 + src/kernel_services/ast_printing/cprint.ml | 1 + src/kernel_services/ast_printing/cprint.mli | 1 + src/kernel_services/ast_queries/cil.ml | 1 + src/kernel_services/ast_queries/cil.mli | 1 + src/kernel_services/ast_queries/cil_builtins.ml | 1 + src/kernel_services/ast_queries/cil_builtins.mli | 1 + src/kernel_services/ast_queries/cil_const.ml | 1 + src/kernel_services/ast_queries/cil_const.mli | 1 + src/kernel_services/parsetree/cabs.ml | 1 + src/kernel_services/parsetree/cabshelper.ml | 1 + src/kernel_services/parsetree/cabshelper.mli | 1 + src/kernel_services/visitors/cabsvisit.ml | 1 + src/kernel_services/visitors/cabsvisit.mli | 1 + src/libraries/utils/cilconfig.ml | 1 + src/libraries/utils/cilconfig.mli | 1 + src/libraries/utils/escape.ml | 1 + src/libraries/utils/escape.mli | 1 + src/plugins/e-acsl/E_ACSL.ml | 1 + src/plugins/e-acsl/E_ACSL.mli | 1 + src/plugins/e-acsl/contrib/libdlmalloc/Makefile | 1 + src/plugins/e-acsl/dune | 1 + src/plugins/e-acsl/dune-project | 1 + src/plugins/e-acsl/man/dune | 1 + src/plugins/e-acsl/man/e-acsl-gcc.sh.1 | 1 + src/plugins/e-acsl/scripts/e-acsl-gcc.sh | 1 + src/plugins/e-acsl/scripts/e-acsl-gcc.sh.comp | 1 + src/plugins/e-acsl/share/e-acsl/e_acsl.h | 1 + src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c | 1 + .../e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c | 1 + .../e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h | 1 + .../share/e-acsl/instrumentation_model/e_acsl_assert_data.h | 1 + .../share/e-acsl/instrumentation_model/e_acsl_assert_data_api.c | 1 + .../share/e-acsl/instrumentation_model/e_acsl_assert_data_api.h | 1 + .../e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.c | 1 + .../e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h | 1 + .../e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.c | 1 + .../e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.h | 1 + .../e-acsl/instrumentation_model/e_acsl_temporal_timestamp.h | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_alias.h | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.c | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.h | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_concurrency.h | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_config.h | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.h | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.c | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h | 1 + .../e-acsl/share/e-acsl/internals/e_acsl_private_assert.c | 1 + .../e-acsl/share/e-acsl/internals/e_acsl_private_assert.h | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_error.c | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_error.h | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_string.c | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_string.h | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.c | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.h | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c | 1 + src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.h | 1 + src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.c | 1 + src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.h | 1 + .../e-acsl/share/e-acsl/libc_replacements/e_acsl_string.c | 1 + .../e-acsl/share/e-acsl/libc_replacements/e_acsl_string.h | 1 + .../e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.c | 1 + .../e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.h | 1 + src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_gmp_api.h | 1 + .../e-acsl/observation_model/bittree_model/e_acsl_bittree.c | 1 + .../e-acsl/observation_model/bittree_model/e_acsl_bittree.h | 1 + .../bittree_model/e_acsl_bittree_observation_model.c | 1 + .../bittree_model/e_acsl_bittree_omodel_debug.c | 1 + .../bittree_model/e_acsl_bittree_timestamp_retrieval.c | 1 + src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.c | 1 + src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.h | 1 + .../share/e-acsl/observation_model/e_acsl_observation_model.c | 1 + .../share/e-acsl/observation_model/e_acsl_observation_model.h | 1 + .../e-acsl/observation_model/internals/e_acsl_heap_tracking.c | 1 + .../e-acsl/observation_model/internals/e_acsl_heap_tracking.h | 1 + .../e-acsl/observation_model/internals/e_acsl_omodel_debug.h | 1 + .../e-acsl/observation_model/internals/e_acsl_patricia_trie.c | 1 + .../e-acsl/observation_model/internals/e_acsl_patricia_trie.h | 1 + .../e-acsl/observation_model/internals/e_acsl_safe_locations.c | 1 + .../e-acsl/observation_model/internals/e_acsl_safe_locations.h | 1 + .../observation_model/internals/e_acsl_timestamp_retrieval.h | 1 + .../segment_model/e_acsl_segment_observation_model.c | 1 + .../segment_model/e_acsl_segment_omodel_debug.c | 1 + .../segment_model/e_acsl_segment_timestamp_retrieval.c | 1 + .../observation_model/segment_model/e_acsl_segment_tracking.c | 1 + .../observation_model/segment_model/e_acsl_segment_tracking.h | 1 + .../observation_model/segment_model/e_acsl_shadow_concurrency.c | 1 + .../observation_model/segment_model/e_acsl_shadow_concurrency.h | 1 + .../observation_model/segment_model/e_acsl_shadow_layout.c | 1 + .../observation_model/segment_model/e_acsl_shadow_layout.h | 1 + src/plugins/e-acsl/src/analyses/analyses.ml | 1 + src/plugins/e-acsl/src/analyses/analyses.mli | 1 + src/plugins/e-acsl/src/analyses/bound_variables.ml | 1 + src/plugins/e-acsl/src/analyses/bound_variables.mli | 1 + src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml | 1 + src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli | 1 + src/plugins/e-acsl/src/analyses/exit_points.ml | 1 + src/plugins/e-acsl/src/analyses/exit_points.mli | 1 + src/plugins/e-acsl/src/analyses/interval.ml | 1 + src/plugins/e-acsl/src/analyses/interval.mli | 1 + src/plugins/e-acsl/src/analyses/labels.ml | 1 + src/plugins/e-acsl/src/analyses/labels.mli | 1 + src/plugins/e-acsl/src/analyses/literal_strings.ml | 1 + src/plugins/e-acsl/src/analyses/literal_strings.mli | 1 + src/plugins/e-acsl/src/analyses/logic_normalizer.ml | 1 + src/plugins/e-acsl/src/analyses/logic_normalizer.mli | 1 + src/plugins/e-acsl/src/analyses/lscope.ml | 1 + src/plugins/e-acsl/src/analyses/lscope.mli | 1 + src/plugins/e-acsl/src/analyses/memory_tracking.ml | 1 + src/plugins/e-acsl/src/analyses/memory_tracking.mli | 1 + src/plugins/e-acsl/src/analyses/rte.ml | 1 + src/plugins/e-acsl/src/analyses/rte.mli | 1 + src/plugins/e-acsl/src/analyses/typing.ml | 1 + src/plugins/e-acsl/src/analyses/typing.mli | 1 + src/plugins/e-acsl/src/analyses/widening.ml | 1 + src/plugins/e-acsl/src/analyses/widening.mli | 1 + src/plugins/e-acsl/src/code_generator/assert.ml | 1 + src/plugins/e-acsl/src/code_generator/assert.mli | 1 + src/plugins/e-acsl/src/code_generator/assigns.ml | 1 + src/plugins/e-acsl/src/code_generator/assigns.mli | 1 + src/plugins/e-acsl/src/code_generator/contract.ml | 1 + src/plugins/e-acsl/src/code_generator/contract.mli | 1 + src/plugins/e-acsl/src/code_generator/contract_types.ml | 1 + src/plugins/e-acsl/src/code_generator/env.ml | 1 + src/plugins/e-acsl/src/code_generator/env.mli | 1 + src/plugins/e-acsl/src/code_generator/global_observer.ml | 1 + src/plugins/e-acsl/src/code_generator/global_observer.mli | 1 + src/plugins/e-acsl/src/code_generator/gmp.ml | 1 + src/plugins/e-acsl/src/code_generator/gmp.mli | 1 + src/plugins/e-acsl/src/code_generator/injector.ml | 1 + src/plugins/e-acsl/src/code_generator/injector.mli | 1 + src/plugins/e-acsl/src/code_generator/libc.ml | 1 + src/plugins/e-acsl/src/code_generator/libc.mli | 1 + src/plugins/e-acsl/src/code_generator/literal_observer.ml | 1 + src/plugins/e-acsl/src/code_generator/literal_observer.mli | 1 + src/plugins/e-acsl/src/code_generator/logic_array.ml | 1 + src/plugins/e-acsl/src/code_generator/logic_array.mli | 1 + src/plugins/e-acsl/src/code_generator/logic_functions.ml | 1 + src/plugins/e-acsl/src/code_generator/logic_functions.mli | 1 + src/plugins/e-acsl/src/code_generator/loops.ml | 1 + src/plugins/e-acsl/src/code_generator/loops.mli | 1 + src/plugins/e-acsl/src/code_generator/memory_observer.ml | 1 + src/plugins/e-acsl/src/code_generator/memory_observer.mli | 1 + src/plugins/e-acsl/src/code_generator/memory_translate.ml | 1 + src/plugins/e-acsl/src/code_generator/memory_translate.mli | 1 + src/plugins/e-acsl/src/code_generator/quantif.ml | 1 + src/plugins/e-acsl/src/code_generator/quantif.mli | 1 + src/plugins/e-acsl/src/code_generator/smart_exp.ml | 1 + src/plugins/e-acsl/src/code_generator/smart_exp.mli | 1 + src/plugins/e-acsl/src/code_generator/smart_stmt.ml | 1 + src/plugins/e-acsl/src/code_generator/smart_stmt.mli | 1 + src/plugins/e-acsl/src/code_generator/temporal.ml | 1 + src/plugins/e-acsl/src/code_generator/temporal.mli | 1 + src/plugins/e-acsl/src/code_generator/translate_annots.ml | 1 + src/plugins/e-acsl/src/code_generator/translate_annots.mli | 1 + src/plugins/e-acsl/src/code_generator/translate_ats.ml | 1 + src/plugins/e-acsl/src/code_generator/translate_ats.mli | 1 + src/plugins/e-acsl/src/code_generator/translate_predicates.ml | 1 + src/plugins/e-acsl/src/code_generator/translate_predicates.mli | 1 + src/plugins/e-acsl/src/code_generator/translate_rtes.ml | 1 + src/plugins/e-acsl/src/code_generator/translate_rtes.mli | 1 + src/plugins/e-acsl/src/code_generator/translate_terms.ml | 1 + src/plugins/e-acsl/src/code_generator/translate_terms.mli | 1 + src/plugins/e-acsl/src/code_generator/translate_utils.ml | 1 + src/plugins/e-acsl/src/code_generator/translate_utils.mli | 1 + src/plugins/e-acsl/src/code_generator/translation_error.ml | 1 + src/plugins/e-acsl/src/code_generator/translation_error.mli | 1 + src/plugins/e-acsl/src/code_generator/typed_number.ml | 1 + src/plugins/e-acsl/src/code_generator/typed_number.mli | 1 + src/plugins/e-acsl/src/dune | 1 + src/plugins/e-acsl/src/libraries/analyses_datatype.ml | 1 + src/plugins/e-acsl/src/libraries/analyses_datatype.mli | 1 + src/plugins/e-acsl/src/libraries/analyses_types.ml | 1 + src/plugins/e-acsl/src/libraries/builtins.ml | 1 + src/plugins/e-acsl/src/libraries/builtins.mli | 1 + src/plugins/e-acsl/src/libraries/error.ml | 1 + src/plugins/e-acsl/src/libraries/error.mli | 1 + src/plugins/e-acsl/src/libraries/functions.ml | 1 + src/plugins/e-acsl/src/libraries/functions.mli | 1 + src/plugins/e-acsl/src/libraries/gmp_types.ml | 1 + src/plugins/e-acsl/src/libraries/gmp_types.mli | 1 + src/plugins/e-acsl/src/libraries/interval_utils.ml | 1 + src/plugins/e-acsl/src/libraries/interval_utils.mli | 1 + src/plugins/e-acsl/src/libraries/logic_aggr.ml | 1 + src/plugins/e-acsl/src/libraries/logic_aggr.mli | 1 + src/plugins/e-acsl/src/libraries/misc.ml | 1 + src/plugins/e-acsl/src/libraries/misc.mli | 1 + src/plugins/e-acsl/src/libraries/varname.ml | 1 + src/plugins/e-acsl/src/libraries/varname.mli | 1 + src/plugins/e-acsl/src/main.ml | 1 + src/plugins/e-acsl/src/main.mli | 1 + src/plugins/e-acsl/src/options.ml | 1 + src/plugins/e-acsl/src/options.mli | 1 + src/plugins/e-acsl/src/project_initializer/prepare_ast.ml | 1 + src/plugins/e-acsl/src/project_initializer/prepare_ast.mli | 1 + src/plugins/e-acsl/src/project_initializer/rtl.ml | 1 + src/plugins/e-acsl/src/project_initializer/rtl.mli | 1 + src/plugins/e-acsl/tab-in-changelog.sh | 1 + src/plugins/e-acsl/tests/E_ACSL_test.ml | 1 + src/plugins/e-acsl/tests/wrapper.sh | 1 + tools/lint/UTF8.ml | 1 + 225 files changed, 225 insertions(+) diff --git a/src/kernel_internals/parsing/clexer.mli b/src/kernel_internals/parsing/clexer.mli index 01635d00e89..8927f15fdd0 100644 --- a/src/kernel_internals/parsing/clexer.mli +++ b/src/kernel_internals/parsing/clexer.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (** The C Lexer. *) diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll index 2e95e6c11da..89dbe33f7d5 100644 --- a/src/kernel_internals/parsing/clexer.mll +++ b/src/kernel_internals/parsing/clexer.mll @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (* FrontC -- lexical analyzer diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly index 0306a989a80..a7f848039f9 100644 --- a/src/kernel_internals/parsing/cparser.mly +++ b/src/kernel_internals/parsing/cparser.mly @@ -39,6 +39,7 @@ /* énergies alternatives) */ /* and INRIA (Institut National de Recherche en Informatique */ /* et Automatique). */ +/* */ /****************************************************************************/ /* 3.22.99 Hugues Cass<E9> First version. diff --git a/src/kernel_internals/parsing/errorloc.ml b/src/kernel_internals/parsing/errorloc.ml index 9d1e3669dce..fcc34938527 100644 --- a/src/kernel_internals/parsing/errorloc.ml +++ b/src/kernel_internals/parsing/errorloc.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (* Copied and modified from [cil/src/errormsg.ml] *) diff --git a/src/kernel_internals/parsing/errorloc.mli b/src/kernel_internals/parsing/errorloc.mli index a83180cd21b..79241282cce 100644 --- a/src/kernel_internals/parsing/errorloc.mli +++ b/src/kernel_internals/parsing/errorloc.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (** The module stores the current file,line, and working directory in a diff --git a/src/kernel_internals/parsing/lexerhack.ml b/src/kernel_internals/parsing/lexerhack.ml index 56f5480b148..00bd71caf96 100644 --- a/src/kernel_internals/parsing/lexerhack.ml +++ b/src/kernel_internals/parsing/lexerhack.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (* We provide here a pointer to a function. It will be set by the lexer and diff --git a/src/kernel_internals/parsing/lexerhack.mli b/src/kernel_internals/parsing/lexerhack.mli index 7be70da71c4..d660b2f4610 100644 --- a/src/kernel_internals/parsing/lexerhack.mli +++ b/src/kernel_internals/parsing/lexerhack.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) val add_identifier: (string -> unit) ref diff --git a/src/kernel_internals/typing/alpha.ml b/src/kernel_internals/typing/alpha.ml index b4d470ca682..73e0f238fac 100644 --- a/src/kernel_internals/typing/alpha.ml +++ b/src/kernel_internals/typing/alpha.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) module H = Hashtbl diff --git a/src/kernel_internals/typing/alpha.mli b/src/kernel_internals/typing/alpha.mli index 075d2f04f5e..36016c46d6a 100644 --- a/src/kernel_internals/typing/alpha.mli +++ b/src/kernel_internals/typing/alpha.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (** Alpha conversion. *) diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 7a2b486adf4..4bac9159e13 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (* Modified by TrustInSoft *) diff --git a/src/kernel_internals/typing/cabs2cil.mli b/src/kernel_internals/typing/cabs2cil.mli index 7ec9c583d59..9ef8d8582ff 100644 --- a/src/kernel_internals/typing/cabs2cil.mli +++ b/src/kernel_internals/typing/cabs2cil.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (** Registers a new hook that will be applied each time a side-effect free diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml index 7da177464c0..25843313a2d 100644 --- a/src/kernel_internals/typing/cfg.ml +++ b/src/kernel_internals/typing/cfg.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (* Authors: Aman Bhargava, S. P. Rahul *) diff --git a/src/kernel_internals/typing/cfg.mli b/src/kernel_internals/typing/cfg.mli index b040cda0b17..6c9f98bda9f 100644 --- a/src/kernel_internals/typing/cfg.mli +++ b/src/kernel_internals/typing/cfg.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (** Code to compute the control-flow graph of a function or file. diff --git a/src/kernel_internals/typing/frontc.ml b/src/kernel_internals/typing/frontc.ml index d48a945dbd9..069bb6bbbb3 100644 --- a/src/kernel_internals/typing/frontc.ml +++ b/src/kernel_internals/typing/frontc.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) let parse_to_cabs (path : Datatype.Filepath.t) = diff --git a/src/kernel_internals/typing/frontc.mli b/src/kernel_internals/typing/frontc.mli index 591aa2013de..34472791f5e 100644 --- a/src/kernel_internals/typing/frontc.mli +++ b/src/kernel_internals/typing/frontc.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (** add a syntactic transformation that will be applied to all freshly parsed diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml index cca4dd7a60f..61b53f17a3c 100644 --- a/src/kernel_internals/typing/mergecil.ml +++ b/src/kernel_internals/typing/mergecil.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (* mergecil.ml *) diff --git a/src/kernel_internals/typing/mergecil.mli b/src/kernel_internals/typing/mergecil.mli index ccde88f5c4e..4532054c22b 100644 --- a/src/kernel_internals/typing/mergecil.mli +++ b/src/kernel_internals/typing/mergecil.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (* diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml index 190753ee6de..c514e975488 100644 --- a/src/kernel_internals/typing/oneret.ml +++ b/src/kernel_internals/typing/oneret.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) open Cil_types diff --git a/src/kernel_internals/typing/oneret.mli b/src/kernel_internals/typing/oneret.mli index 845c74dc833..de5b46fc81d 100644 --- a/src/kernel_internals/typing/oneret.mli +++ b/src/kernel_internals/typing/oneret.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (* diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml index c07bfae94a5..01c1b346c1d 100644 --- a/src/kernel_internals/typing/rmtmps.ml +++ b/src/kernel_internals/typing/rmtmps.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) let dkey = Kernel.dkey_rmtmps diff --git a/src/kernel_internals/typing/rmtmps.mli b/src/kernel_internals/typing/rmtmps.mli index 015a4f4dff3..3693448008d 100644 --- a/src/kernel_internals/typing/rmtmps.mli +++ b/src/kernel_internals/typing/rmtmps.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (* rmtmps.mli *) diff --git a/src/kernel_services/analysis/dataflows.ml b/src/kernel_services/analysis/dataflows.ml index 8f0dde14978..ffd8a27cd30 100644 --- a/src/kernel_services/analysis/dataflows.ml +++ b/src/kernel_services/analysis/dataflows.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) open Ordered_stmt diff --git a/src/kernel_services/analysis/dataflows.mli b/src/kernel_services/analysis/dataflows.mli index 438d16c03b7..70127054853 100644 --- a/src/kernel_services/analysis/dataflows.mli +++ b/src/kernel_services/analysis/dataflows.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (** Implementation of data flow analyses over user-supplied domains. *) diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml index 8cb7318ad07..d1e72d54804 100644 --- a/src/kernel_services/ast_data/cil_types.ml +++ b/src/kernel_services/ast_data/cil_types.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (** The Abstract Syntax of CIL. diff --git a/src/kernel_services/ast_printing/cprint.ml b/src/kernel_services/ast_printing/cprint.ml index b9de6911561..726864b24c3 100644 --- a/src/kernel_services/ast_printing/cprint.ml +++ b/src/kernel_services/ast_printing/cprint.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (* cprint -- pretty printer of C program from abstract syntax diff --git a/src/kernel_services/ast_printing/cprint.mli b/src/kernel_services/ast_printing/cprint.mli index 448ad7258a1..9c1c948629a 100644 --- a/src/kernel_services/ast_printing/cprint.mli +++ b/src/kernel_services/ast_printing/cprint.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (** Printers for the Cabs AST *) diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index e287cf0048d..449f772b287 100644 --- a/src/kernel_services/ast_queries/cil.ml +++ b/src/kernel_services/ast_queries/cil.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (* Modified by TrustInSoft *) diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli index ca938f4a42d..480b1edd994 100644 --- a/src/kernel_services/ast_queries/cil.mli +++ b/src/kernel_services/ast_queries/cil.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (** CIL main API. diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml index c80b32e7484..fe00e5c8871 100644 --- a/src/kernel_services/ast_queries/cil_builtins.ml +++ b/src/kernel_services/ast_queries/cil_builtins.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) open Cil_datatype diff --git a/src/kernel_services/ast_queries/cil_builtins.mli b/src/kernel_services/ast_queries/cil_builtins.mli index 45b02173c47..f822966b9ca 100644 --- a/src/kernel_services/ast_queries/cil_builtins.mli +++ b/src/kernel_services/ast_queries/cil_builtins.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) open Cil_types diff --git a/src/kernel_services/ast_queries/cil_const.ml b/src/kernel_services/ast_queries/cil_const.ml index 74176389529..bd4d41d64ce 100644 --- a/src/kernel_services/ast_queries/cil_const.ml +++ b/src/kernel_services/ast_queries/cil_const.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) open Cil_types diff --git a/src/kernel_services/ast_queries/cil_const.mli b/src/kernel_services/ast_queries/cil_const.mli index 47f7659a34e..5edd0ba2b30 100644 --- a/src/kernel_services/ast_queries/cil_const.mli +++ b/src/kernel_services/ast_queries/cil_const.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (** Smart constructors for some CIL data types *) diff --git a/src/kernel_services/parsetree/cabs.ml b/src/kernel_services/parsetree/cabs.ml index 9b45e7218e3..bf4c553242b 100644 --- a/src/kernel_services/parsetree/cabs.ml +++ b/src/kernel_services/parsetree/cabs.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (** Untyped AST. diff --git a/src/kernel_services/parsetree/cabshelper.ml b/src/kernel_services/parsetree/cabshelper.ml index f575cd30f71..e557a91dd58 100644 --- a/src/kernel_services/parsetree/cabshelper.ml +++ b/src/kernel_services/parsetree/cabshelper.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) open Cabs diff --git a/src/kernel_services/parsetree/cabshelper.mli b/src/kernel_services/parsetree/cabshelper.mli index 5485c1b5837..1b1fbfc418e 100644 --- a/src/kernel_services/parsetree/cabshelper.mli +++ b/src/kernel_services/parsetree/cabshelper.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (** Helper functions for Cabs *) diff --git a/src/kernel_services/visitors/cabsvisit.ml b/src/kernel_services/visitors/cabsvisit.ml index 357a69cd097..d5a7fe9ae3d 100644 --- a/src/kernel_services/visitors/cabsvisit.ml +++ b/src/kernel_services/visitors/cabsvisit.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (* cabsvisit.ml *) diff --git a/src/kernel_services/visitors/cabsvisit.mli b/src/kernel_services/visitors/cabsvisit.mli index 0714cf8e4fc..253492ab625 100644 --- a/src/kernel_services/visitors/cabsvisit.mli +++ b/src/kernel_services/visitors/cabsvisit.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (* cabsvisit.mli *) diff --git a/src/libraries/utils/cilconfig.ml b/src/libraries/utils/cilconfig.ml index 4b479e985f7..844ea8a1c4d 100644 --- a/src/libraries/utils/cilconfig.ml +++ b/src/libraries/utils/cilconfig.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) module H = Hashtbl diff --git a/src/libraries/utils/cilconfig.mli b/src/libraries/utils/cilconfig.mli index ab249296474..46e5a7b3441 100644 --- a/src/libraries/utils/cilconfig.mli +++ b/src/libraries/utils/cilconfig.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) diff --git a/src/libraries/utils/escape.ml b/src/libraries/utils/escape.ml index bed960e171c..bb4b73c8071 100644 --- a/src/libraries/utils/escape.ml +++ b/src/libraries/utils/escape.ml @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) diff --git a/src/libraries/utils/escape.mli b/src/libraries/utils/escape.mli index d43bb622df4..49ef2c2cfb6 100644 --- a/src/libraries/utils/escape.mli +++ b/src/libraries/utils/escape.mli @@ -39,6 +39,7 @@ (* énergies alternatives) *) (* and INRIA (Institut National de Recherche en Informatique *) (* et Automatique). *) +(* *) (****************************************************************************) (* diff --git a/src/plugins/e-acsl/E_ACSL.ml b/src/plugins/e-acsl/E_ACSL.ml index 33ff9ca86af..f8fdc67b847 100644 --- a/src/plugins/e-acsl/E_ACSL.ml +++ b/src/plugins/e-acsl/E_ACSL.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** E-ACSL. *) diff --git a/src/plugins/e-acsl/E_ACSL.mli b/src/plugins/e-acsl/E_ACSL.mli index 8c82c12a072..22530abf4e3 100644 --- a/src/plugins/e-acsl/E_ACSL.mli +++ b/src/plugins/e-acsl/E_ACSL.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** E-ACSL. *) diff --git a/src/plugins/e-acsl/contrib/libdlmalloc/Makefile b/src/plugins/e-acsl/contrib/libdlmalloc/Makefile index e97b013d748..b62a71fb7be 100644 --- a/src/plugins/e-acsl/contrib/libdlmalloc/Makefile +++ b/src/plugins/e-acsl/contrib/libdlmalloc/Makefile @@ -17,6 +17,7 @@ # # # See the GNU Lesser General Public License version 2.1 # # for more details (enclosed in the file licenses/LGPLv2.1). # +# # ########################################################################## EACSL_DLMALLOC_LIB = libeacsl-dlmalloc.a diff --git a/src/plugins/e-acsl/dune b/src/plugins/e-acsl/dune index bf40e08f3b4..2a14f54f6fe 100644 --- a/src/plugins/e-acsl/dune +++ b/src/plugins/e-acsl/dune @@ -17,6 +17,7 @@ ;; ;; ;; See the GNU Lesser General Public License version 2.1 ;; ;; for more details (enclosed in the file licenses/LGPLv2.1). ;; +;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; BUILD LIBDLMALLOC diff --git a/src/plugins/e-acsl/dune-project b/src/plugins/e-acsl/dune-project index 2412c3af493..94c9af22061 100644 --- a/src/plugins/e-acsl/dune-project +++ b/src/plugins/e-acsl/dune-project @@ -18,6 +18,7 @@ ;; ;; ;; See the GNU Lesser General Public License version 2.1 ;; ;; for more details (enclosed in the file licenses/LGPLv2.1). ;; +;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (name frama-c-e-acsl) diff --git a/src/plugins/e-acsl/man/dune b/src/plugins/e-acsl/man/dune index 55ff6d1f41a..f2032a3f4b6 100644 --- a/src/plugins/e-acsl/man/dune +++ b/src/plugins/e-acsl/man/dune @@ -17,6 +17,7 @@ ;; ;; ;; See the GNU Lesser General Public License version 2.1 ;; ;; for more details (enclosed in the file licenses/LGPLv2.1). ;; +;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (install diff --git a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 index 8134e9d4d13..178b88e50eb 100644 --- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 +++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 @@ -17,6 +17,7 @@ .\" .\" See the GNU Lesser General Public License version 2.1 .\" for more details (enclosed in the file licenses/LGPLv2.1). +.\" .\"------------------------------------------------------------------------ .TH E-ACSL-GCC.SH 1 2016-02-02 diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index aebdb3e7af2..68880f34d54 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh @@ -18,6 +18,7 @@ # # # See the GNU Lesser General Public License version 2.1 # # for more details (enclosed in the file licenses/LGPLv2.1). # +# # ########################################################################## # Convenience wrapper for small runs of E-ACSL Frama-C plugin diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh.comp b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh.comp index 19d26ed1a6c..75680227787 100644 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh.comp +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh.comp @@ -17,6 +17,7 @@ # # # See the GNU Lesser General Public License version 2.1 # # for more details (enclosed in the file licenses/LGPLv2.1). # +# # ########################################################################## # Bash completion for e-acsl-gcc.sh diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl.h b/src/plugins/e-acsl/share/e-acsl/e_acsl.h index f42d66cf2ff..b079b277f4a 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c b/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c index e5021d0957b..527bf92f873 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /* Get default definitions and macros e.g., PATH_MAX */ diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c index aad9fe434ce..64dc07cd8d5 100644 --- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c +++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h index 01dd86b4ceb..2da8074614b 100644 --- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h +++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data.h b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data.h index 9f226600483..5edc65de912 100644 --- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data.h +++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data_api.c b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data_api.c index 6c1511b6661..d185800c9a4 100644 --- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data_api.c +++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data_api.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data_api.h b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data_api.h index 9839c6d8c7c..be923d8b0c9 100644 --- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data_api.h +++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data_api.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.c b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.c index d27601ba871..afc65fba6aa 100644 --- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.c +++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h index c7052319607..b42822c4355 100644 --- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h +++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.c b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.c index eb77a8f1f82..dbdb9149934 100644 --- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.c +++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #ifdef E_ACSL_TEMPORAL diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.h b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.h index eb9f8704913..5f2dca0019e 100644 --- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.h +++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal_timestamp.h b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal_timestamp.h index 5b1c40d9fa9..57188c4e538 100644 --- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal_timestamp.h +++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal_timestamp.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_alias.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_alias.h index 91abbc87f4b..1a5fa47767a 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_alias.h +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_alias.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.c index 5d290017d6c..460cbf84116 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.c +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include "e_acsl_bits.h" diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.h index ba0c7192892..b91c527dedf 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.h +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_bits.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_concurrency.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_concurrency.h index d06986c072c..d28cdf3b240 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_concurrency.h +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_concurrency.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_config.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_config.h index 15363446820..58d1d0e75aa 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_config.h +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_config.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c index e2e2305bdab..fe2eb4d129f 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include <fcntl.h> diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.h index ff95d1bbb43..b45b8e401d3 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.h +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.c index 6b43504d6bb..2b6d9b1e8e7 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.c +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include "e_acsl_malloc.h" diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h index 0207295a096..36ee84d817b 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c index ffd83e5dac7..c43e70533af 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include <limits.h> diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.h index 67629be93cb..6be16c0d038 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.h +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_error.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_error.c index f895ac6e534..f3e7ae744e9 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_error.c +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_error.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_error.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_error.h index 4e56849d152..f6cdf591efb 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_error.h +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_error.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_string.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_string.c index 01fad25c2c4..967a8b71193 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_string.c +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_string.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include "e_acsl_malloc.h" diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_string.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_string.h index 765580e7cd6..2f64176d07c 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_string.h +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_string.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.c index aab766203ab..1d662b4a68f 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.c +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.h index 12dd32684be..961eee807ed 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.h +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c index dacc26be6cb..143c156d8fe 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /* Get default definitions and macros e.g., PATH_MAX */ diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.h index 6850b6bc87e..3a6e5f605c9 100644 --- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.h +++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.c b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.c index 1624788d622..94dbd3af8a0 100644 --- a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.c +++ b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #ifdef E_ACSL_VALIDATE_FORMAT_STRINGS diff --git a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.h b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.h index 02c1eb16329..d63cf3f6c20 100644 --- a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.h +++ b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.c b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.c index c502b7f8f81..74eb6da11a7 100644 --- a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.c +++ b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include "../internals/e_acsl_private_assert.h" diff --git a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.h b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.h index db4b90f1735..16b97a9407e 100644 --- a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.h +++ b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.c b/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.c index adb5beebea3..6e2d0e4a0a9 100644 --- a/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.c +++ b/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include <fenv.h> diff --git a/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.h b/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.h index 5b353dd3c20..c4583bf43e6 100644 --- a/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.h +++ b/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_gmp_api.h b/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_gmp_api.h index d21e842803f..ccd6d8751b6 100644 --- a/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_gmp_api.h +++ b/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_gmp_api.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c index 77eb3a9f77a..80e20bc5a3a 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.h b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.h index 163adb9f7c6..84d2a0c483a 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.h +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c index 89385d53944..a1e7b0c7ed0 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c index bee026068b0..05b299ab2e2 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include "../../internals/e_acsl_private_assert.h" diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_timestamp_retrieval.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_timestamp_retrieval.c index 84167a1c878..86538ebfa9d 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_timestamp_retrieval.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_timestamp_retrieval.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include "../../internals/e_acsl_private_assert.h" diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.c b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.c index e13bae1d36a..a288e527f70 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include "internals/e_acsl_heap_tracking.h" diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.h b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.h index e30cc710442..99c12fb6b04 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.h +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c index 376c3ab19c3..b962116adb9 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /************************************************************************/ diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h index 1ef49697594..38737179123 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.c b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.c index 70d8de1e094..266402332d5 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include "e_acsl_heap_tracking.h" diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.h b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.h index de2402bb286..03fe0e123d0 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.h +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_omodel_debug.h b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_omodel_debug.h index 892321163ae..e790aae88eb 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_omodel_debug.h +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_omodel_debug.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #ifndef E_ACSL_OMODEL_DEBUG_H diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c index 417e9ddc60f..f887b0ca259 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h index 5a529f64b44..f7830b4eff6 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_patricia_trie.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c index 2a8d47fdac6..64fb1fd55b7 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include <errno.h> diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h index f80ed42bf1d..434e741b326 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_timestamp_retrieval.h b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_timestamp_retrieval.h index 39856c36c16..8f6af007add 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_timestamp_retrieval.h +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_timestamp_retrieval.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c index 7bb0944f858..ebd6635e722 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c index 37a0b4132f0..4c63638e2ce 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include "../../internals/e_acsl_bits.h" diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_timestamp_retrieval.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_timestamp_retrieval.c index 9e871b02dde..f52896f3b23 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_timestamp_retrieval.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_timestamp_retrieval.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include "e_acsl_segment_tracking.h" diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c index c92ba0da83c..107dbd0bc32 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include <inttypes.h> diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h index b4add2bf221..f8c2f8a1da7 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c index 4ffd003425a..b6e4b1643d6 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.h b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.h index 7a8feed4aae..c7699522065 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.h +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c index c9a0cfb3c00..a25bbcaa889 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ #include <stddef.h> diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h index e340b543f4d..9e1abdec36a 100644 --- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h +++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h @@ -17,6 +17,7 @@ /* */ /* See the GNU Lesser General Public License version 2.1 */ /* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ /**************************************************************************/ /*! *********************************************************************** diff --git a/src/plugins/e-acsl/src/analyses/analyses.ml b/src/plugins/e-acsl/src/analyses/analyses.ml index 94f2d17dfe4..cc0bcb14054 100644 --- a/src/plugins/e-acsl/src/analyses/analyses.ml +++ b/src/plugins/e-acsl/src/analyses/analyses.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) let analyses_feedback msg = diff --git a/src/plugins/e-acsl/src/analyses/analyses.mli b/src/plugins/e-acsl/src/analyses/analyses.mli index 6b8658b6304..6125f7fdd77 100644 --- a/src/plugins/e-acsl/src/analyses/analyses.mli +++ b/src/plugins/e-acsl/src/analyses/analyses.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** General module for E-ACSL analyses *) diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml index 134f204adc3..441dadd082b 100644 --- a/src/plugins/e-acsl/src/analyses/bound_variables.ml +++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Module for preprocessing the quantified predicates. Predicates with diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.mli b/src/plugins/e-acsl/src/analyses/bound_variables.mli index 8d61c7eeaee..e8a99e37bc1 100644 --- a/src/plugins/e-acsl/src/analyses/bound_variables.mli +++ b/src/plugins/e-acsl/src/analyses/bound_variables.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml index fb0426730ff..8674b84187c 100644 --- a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml +++ b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli index 5ea8af8b0d4..9189cf59833 100644 --- a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli +++ b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/analyses/exit_points.ml b/src/plugins/e-acsl/src/analyses/exit_points.ml index 3ea0b45ba81..dea92c70b09 100644 --- a/src/plugins/e-acsl/src/analyses/exit_points.ml +++ b/src/plugins/e-acsl/src/analyses/exit_points.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/analyses/exit_points.mli b/src/plugins/e-acsl/src/analyses/exit_points.mli index 1061c1027db..732e7b92e38 100644 --- a/src/plugins/e-acsl/src/analyses/exit_points.mli +++ b/src/plugins/e-acsl/src/analyses/exit_points.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** E-ACSL tracks a local variable by injecting: diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml index 5c783b65c68..d43be59cca8 100644 --- a/src/plugins/e-acsl/src/analyses/interval.ml +++ b/src/plugins/e-acsl/src/analyses/interval.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/analyses/interval.mli b/src/plugins/e-acsl/src/analyses/interval.mli index 64aaf7efe1f..1cbc7492730 100644 --- a/src/plugins/e-acsl/src/analyses/interval.mli +++ b/src/plugins/e-acsl/src/analyses/interval.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Interval inference for terms. diff --git a/src/plugins/e-acsl/src/analyses/labels.ml b/src/plugins/e-acsl/src/analyses/labels.ml index 26284e02a9b..afca5076f37 100644 --- a/src/plugins/e-acsl/src/analyses/labels.ml +++ b/src/plugins/e-acsl/src/analyses/labels.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Pre-analysis for Labeled terms and predicates. *) diff --git a/src/plugins/e-acsl/src/analyses/labels.mli b/src/plugins/e-acsl/src/analyses/labels.mli index e34ca1b9ca8..1c9a7951d7f 100644 --- a/src/plugins/e-acsl/src/analyses/labels.mli +++ b/src/plugins/e-acsl/src/analyses/labels.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Pre-analysis for Labeled terms and predicates. diff --git a/src/plugins/e-acsl/src/analyses/literal_strings.ml b/src/plugins/e-acsl/src/analyses/literal_strings.ml index 9bb5945b338..60c0c4042c5 100644 --- a/src/plugins/e-acsl/src/analyses/literal_strings.ml +++ b/src/plugins/e-acsl/src/analyses/literal_strings.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/analyses/literal_strings.mli b/src/plugins/e-acsl/src/analyses/literal_strings.mli index 63a861b9874..5a83b3e7181 100644 --- a/src/plugins/e-acsl/src/analyses/literal_strings.mli +++ b/src/plugins/e-acsl/src/analyses/literal_strings.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Associate literal strings to fresh varinfo. *) diff --git a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml index e5c812b7fe9..8e370f5f25c 100644 --- a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml +++ b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/analyses/logic_normalizer.mli b/src/plugins/e-acsl/src/analyses/logic_normalizer.mli index 3b82697abda..521d23380fd 100644 --- a/src/plugins/e-acsl/src/analyses/logic_normalizer.mli +++ b/src/plugins/e-acsl/src/analyses/logic_normalizer.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** This module is dedicated to some preprocessing on the predicates: diff --git a/src/plugins/e-acsl/src/analyses/lscope.ml b/src/plugins/e-acsl/src/analyses/lscope.ml index 3b77b35298c..75ad1069a99 100644 --- a/src/plugins/e-acsl/src/analyses/lscope.ml +++ b/src/plugins/e-acsl/src/analyses/lscope.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/analyses/lscope.mli b/src/plugins/e-acsl/src/analyses/lscope.mli index 986809620ed..3a603d8c2fd 100644 --- a/src/plugins/e-acsl/src/analyses/lscope.mli +++ b/src/plugins/e-acsl/src/analyses/lscope.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Analyses_types diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml index b5d25f7b0f0..c9dafda541a 100644 --- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml +++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.mli b/src/plugins/e-acsl/src/analyses/memory_tracking.mli index 7bd06d4d703..7506e46adf9 100644 --- a/src/plugins/e-acsl/src/analyses/memory_tracking.mli +++ b/src/plugins/e-acsl/src/analyses/memory_tracking.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/analyses/rte.ml b/src/plugins/e-acsl/src/analyses/rte.ml index 9cef65315ab..2aa4d49bcbc 100644 --- a/src/plugins/e-acsl/src/analyses/rte.ml +++ b/src/plugins/e-acsl/src/analyses/rte.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (* ************************************************************************** *) diff --git a/src/plugins/e-acsl/src/analyses/rte.mli b/src/plugins/e-acsl/src/analyses/rte.mli index e2083cddc3b..0f307c8ef51 100644 --- a/src/plugins/e-acsl/src/analyses/rte.mli +++ b/src/plugins/e-acsl/src/analyses/rte.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Accessing the RTE plug-in easily. *) diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml index 92a04aa78e4..99d59523258 100644 --- a/src/plugins/e-acsl/src/analyses/typing.ml +++ b/src/plugins/e-acsl/src/analyses/typing.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli index f0892609647..b0dcc3e9fde 100644 --- a/src/plugins/e-acsl/src/analyses/typing.mli +++ b/src/plugins/e-acsl/src/analyses/typing.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Type system which computes the smallest C type that may contain all the diff --git a/src/plugins/e-acsl/src/analyses/widening.ml b/src/plugins/e-acsl/src/analyses/widening.ml index 40246542e69..96801eb7237 100644 --- a/src/plugins/e-acsl/src/analyses/widening.ml +++ b/src/plugins/e-acsl/src/analyses/widening.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/analyses/widening.mli b/src/plugins/e-acsl/src/analyses/widening.mli index df35d6deb45..36fd4dc0868 100644 --- a/src/plugins/e-acsl/src/analyses/widening.mli +++ b/src/plugins/e-acsl/src/analyses/widening.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/assert.ml b/src/plugins/e-acsl/src/code_generator/assert.ml index 24685560a90..a49425e216c 100644 --- a/src/plugins/e-acsl/src/code_generator/assert.ml +++ b/src/plugins/e-acsl/src/code_generator/assert.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Module with the context to hold the data contributing to an assertion and diff --git a/src/plugins/e-acsl/src/code_generator/assert.mli b/src/plugins/e-acsl/src/code_generator/assert.mli index 4a2b6640692..fd98f26c87d 100644 --- a/src/plugins/e-acsl/src/code_generator/assert.mli +++ b/src/plugins/e-acsl/src/code_generator/assert.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Module with the context to hold the data contributing to an assertion and diff --git a/src/plugins/e-acsl/src/code_generator/assigns.ml b/src/plugins/e-acsl/src/code_generator/assigns.ml index 1be38110706..f33b65bf6e1 100644 --- a/src/plugins/e-acsl/src/code_generator/assigns.ml +++ b/src/plugins/e-acsl/src/code_generator/assigns.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/assigns.mli b/src/plugins/e-acsl/src/code_generator/assigns.mli index 35aba7352d0..2d4d110177e 100644 --- a/src/plugins/e-acsl/src/code_generator/assigns.mli +++ b/src/plugins/e-acsl/src/code_generator/assigns.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) exception NoAssigns diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml index 5a5bc3ba4b4..e7118a6f17f 100644 --- a/src/plugins/e-acsl/src/code_generator/contract.ml +++ b/src/plugins/e-acsl/src/code_generator/contract.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/contract.mli b/src/plugins/e-acsl/src/code_generator/contract.mli index afc1a4899a0..a6eb339b270 100644 --- a/src/plugins/e-acsl/src/code_generator/contract.mli +++ b/src/plugins/e-acsl/src/code_generator/contract.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/contract_types.ml b/src/plugins/e-acsl/src/code_generator/contract_types.ml index 96975ee7ea2..f3164dd39ee 100644 --- a/src/plugins/e-acsl/src/code_generator/contract_types.ml +++ b/src/plugins/e-acsl/src/code_generator/contract_types.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml index a375e446ed5..bd8614fe577 100644 --- a/src/plugins/e-acsl/src/code_generator/env.ml +++ b/src/plugins/e-acsl/src/code_generator/env.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli index 926121b0f6f..91d3aed298a 100644 --- a/src/plugins/e-acsl/src/code_generator/env.mli +++ b/src/plugins/e-acsl/src/code_generator/env.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.ml b/src/plugins/e-acsl/src/code_generator/global_observer.ml index 5534f414680..847b8d042df 100644 --- a/src/plugins/e-acsl/src/code_generator/global_observer.ml +++ b/src/plugins/e-acsl/src/code_generator/global_observer.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.mli b/src/plugins/e-acsl/src/code_generator/global_observer.mli index 3ae26d16f1d..c33dbeacca2 100644 --- a/src/plugins/e-acsl/src/code_generator/global_observer.mli +++ b/src/plugins/e-acsl/src/code_generator/global_observer.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Observation of global variables. *) diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml index 7c3d6a99408..4e0bd136867 100644 --- a/src/plugins/e-acsl/src/code_generator/gmp.ml +++ b/src/plugins/e-acsl/src/code_generator/gmp.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/gmp.mli b/src/plugins/e-acsl/src/code_generator/gmp.mli index da355f9a644..f37a85513f8 100644 --- a/src/plugins/e-acsl/src/code_generator/gmp.mli +++ b/src/plugins/e-acsl/src/code_generator/gmp.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Calls to the GMP's API. *) diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml index ebfa6916e47..a1b7e026977 100644 --- a/src/plugins/e-acsl/src/code_generator/injector.ml +++ b/src/plugins/e-acsl/src/code_generator/injector.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/injector.mli b/src/plugins/e-acsl/src/code_generator/injector.mli index a3c6d20babd..bee2c6ecd29 100644 --- a/src/plugins/e-acsl/src/code_generator/injector.mli +++ b/src/plugins/e-acsl/src/code_generator/injector.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** The E-ACSL main instrumentation step. *) diff --git a/src/plugins/e-acsl/src/code_generator/libc.ml b/src/plugins/e-acsl/src/code_generator/libc.ml index ba4ace743e0..9e34bde8fd6 100644 --- a/src/plugins/e-acsl/src/code_generator/libc.ml +++ b/src/plugins/e-acsl/src/code_generator/libc.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Code generation for libc functions *) diff --git a/src/plugins/e-acsl/src/code_generator/libc.mli b/src/plugins/e-acsl/src/code_generator/libc.mli index fa7be849cde..8c99f8bab92 100644 --- a/src/plugins/e-acsl/src/code_generator/libc.mli +++ b/src/plugins/e-acsl/src/code_generator/libc.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Code generation for libc functions *) diff --git a/src/plugins/e-acsl/src/code_generator/literal_observer.ml b/src/plugins/e-acsl/src/code_generator/literal_observer.ml index 16dd3dfcf59..37ee1d9fb9e 100644 --- a/src/plugins/e-acsl/src/code_generator/literal_observer.ml +++ b/src/plugins/e-acsl/src/code_generator/literal_observer.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/literal_observer.mli b/src/plugins/e-acsl/src/code_generator/literal_observer.mli index 46cf003e820..dbb9be9df4c 100644 --- a/src/plugins/e-acsl/src/code_generator/literal_observer.mli +++ b/src/plugins/e-acsl/src/code_generator/literal_observer.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Observation of literal strings in C expressions. *) diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.ml b/src/plugins/e-acsl/src/code_generator/logic_array.ml index 068a850b315..6d9ba8fad8f 100644 --- a/src/plugins/e-acsl/src/code_generator/logic_array.ml +++ b/src/plugins/e-acsl/src/code_generator/logic_array.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.mli b/src/plugins/e-acsl/src/code_generator/logic_array.mli index bf95f50478e..2ca72559257 100644 --- a/src/plugins/e-acsl/src/code_generator/logic_array.mli +++ b/src/plugins/e-acsl/src/code_generator/logic_array.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml index 8db12b5daad..421a71f5527 100644 --- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml +++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.mli b/src/plugins/e-acsl/src/code_generator/logic_functions.mli index a242fd62573..73eef16200f 100644 --- a/src/plugins/e-acsl/src/code_generator/logic_functions.mli +++ b/src/plugins/e-acsl/src/code_generator/logic_functions.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml index 3a7d1e91a72..10fc89d0512 100644 --- a/src/plugins/e-acsl/src/code_generator/loops.ml +++ b/src/plugins/e-acsl/src/code_generator/loops.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil diff --git a/src/plugins/e-acsl/src/code_generator/loops.mli b/src/plugins/e-acsl/src/code_generator/loops.mli index 9d0b2d778d8..614eb9a2373 100644 --- a/src/plugins/e-acsl/src/code_generator/loops.mli +++ b/src/plugins/e-acsl/src/code_generator/loops.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Loop specific actions. *) diff --git a/src/plugins/e-acsl/src/code_generator/memory_observer.ml b/src/plugins/e-acsl/src/code_generator/memory_observer.ml index 2b188fb13ea..b911ca68f95 100644 --- a/src/plugins/e-acsl/src/code_generator/memory_observer.ml +++ b/src/plugins/e-acsl/src/code_generator/memory_observer.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_datatype diff --git a/src/plugins/e-acsl/src/code_generator/memory_observer.mli b/src/plugins/e-acsl/src/code_generator/memory_observer.mli index 92ce43ff263..8153bc4f514 100644 --- a/src/plugins/e-acsl/src/code_generator/memory_observer.mli +++ b/src/plugins/e-acsl/src/code_generator/memory_observer.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Extend the environment with statements which allocate/deallocate memory diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml index 28a43d32fa6..84de94e2d1e 100644 --- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml +++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.mli b/src/plugins/e-acsl/src/code_generator/memory_translate.mli index f4cec24ff8e..5445759ebc6 100644 --- a/src/plugins/e-acsl/src/code_generator/memory_translate.mli +++ b/src/plugins/e-acsl/src/code_generator/memory_translate.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml index 9b7057239cd..a851389f548 100644 --- a/src/plugins/e-acsl/src/code_generator/quantif.ml +++ b/src/plugins/e-acsl/src/code_generator/quantif.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/quantif.mli b/src/plugins/e-acsl/src/code_generator/quantif.mli index 99427f4527e..b0d24f004c3 100644 --- a/src/plugins/e-acsl/src/code_generator/quantif.mli +++ b/src/plugins/e-acsl/src/code_generator/quantif.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Convert quantifiers. *) diff --git a/src/plugins/e-acsl/src/code_generator/smart_exp.ml b/src/plugins/e-acsl/src/code_generator/smart_exp.ml index 2a1562aa0b6..dc5a6cc5fa0 100644 --- a/src/plugins/e-acsl/src/code_generator/smart_exp.ml +++ b/src/plugins/e-acsl/src/code_generator/smart_exp.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/smart_exp.mli b/src/plugins/e-acsl/src/code_generator/smart_exp.mli index ed3f2cd1fbd..7764038cba1 100644 --- a/src/plugins/e-acsl/src/code_generator/smart_exp.mli +++ b/src/plugins/e-acsl/src/code_generator/smart_exp.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml index 7bc50a2282d..ede8d77c78b 100644 --- a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml +++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli index 3ddeda1f934..f2e49c875c1 100644 --- a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli +++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/temporal.ml b/src/plugins/e-acsl/src/code_generator/temporal.ml index 3e4f4ecc7e5..621e54993c5 100644 --- a/src/plugins/e-acsl/src/code_generator/temporal.ml +++ b/src/plugins/e-acsl/src/code_generator/temporal.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (* Detailed description of transformations implemented in this file is diff --git a/src/plugins/e-acsl/src/code_generator/temporal.mli b/src/plugins/e-acsl/src/code_generator/temporal.mli index 9f2a075415c..8958a8cab1c 100644 --- a/src/plugins/e-acsl/src/code_generator/temporal.mli +++ b/src/plugins/e-acsl/src/code_generator/temporal.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Transformations to detect temporal memory errors (e.g., dereference of diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.ml b/src/plugins/e-acsl/src/code_generator/translate_annots.ml index e2b6b1ee315..439c2dba354 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml +++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.mli b/src/plugins/e-acsl/src/code_generator/translate_annots.mli index 26dee7eb9e5..f115d34fc14 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_annots.mli +++ b/src/plugins/e-acsl/src/code_generator/translate_annots.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml index 4cdb9e9e224..961e4a5bae7 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml +++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Generate C implementations of E-ACSL [\at()] terms and predicates. *) diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.mli b/src/plugins/e-acsl/src/code_generator/translate_ats.mli index 9307257a535..dffc18437ac 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_ats.mli +++ b/src/plugins/e-acsl/src/code_generator/translate_ats.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Generate C implementations of E-ACSL [\at()] terms and predicates. *) diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml index 9f9190ba290..220e628d43d 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml +++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Generate C implementations of E-ACSL predicates. *) diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.mli b/src/plugins/e-acsl/src/code_generator/translate_predicates.mli index 57808e08577..d32971917c5 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_predicates.mli +++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml index d17e6dbf3a6..239e3707b4a 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml +++ b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Generate and translate RTE annotations. *) diff --git a/src/plugins/e-acsl/src/code_generator/translate_rtes.mli b/src/plugins/e-acsl/src/code_generator/translate_rtes.mli index 300b8467488..06cf6fa5957 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_rtes.mli +++ b/src/plugins/e-acsl/src/code_generator/translate_rtes.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml index d252cfced7b..579ccf28683 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml +++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Generate C implementations of E-ACSL terms. *) diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.mli b/src/plugins/e-acsl/src/code_generator/translate_terms.mli index 6b5d18cd8ca..309687cfdec 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_terms.mli +++ b/src/plugins/e-acsl/src/code_generator/translate_terms.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.ml b/src/plugins/e-acsl/src/code_generator/translate_utils.ml index 2ae9246a87e..ee84ecdca58 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_utils.ml +++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Utility functions for generating C implementations. *) diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.mli b/src/plugins/e-acsl/src/code_generator/translate_utils.mli index 44a437bc50a..81190863ccd 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_utils.mli +++ b/src/plugins/e-acsl/src/code_generator/translate_utils.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/code_generator/translation_error.ml b/src/plugins/e-acsl/src/code_generator/translation_error.ml index d6084712f8f..aa40e3d5183 100644 --- a/src/plugins/e-acsl/src/code_generator/translation_error.ml +++ b/src/plugins/e-acsl/src/code_generator/translation_error.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) include Error.Make(struct let phase = Options.Dkey.translation end) diff --git a/src/plugins/e-acsl/src/code_generator/translation_error.mli b/src/plugins/e-acsl/src/code_generator/translation_error.mli index 285f7313019..60db3c3beef 100644 --- a/src/plugins/e-acsl/src/code_generator/translation_error.mli +++ b/src/plugins/e-acsl/src/code_generator/translation_error.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) include Error.S diff --git a/src/plugins/e-acsl/src/code_generator/typed_number.ml b/src/plugins/e-acsl/src/code_generator/typed_number.ml index ef68ea8861e..ab7f78841fd 100644 --- a/src/plugins/e-acsl/src/code_generator/typed_number.ml +++ b/src/plugins/e-acsl/src/code_generator/typed_number.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Manipulate the type of numbers. *) diff --git a/src/plugins/e-acsl/src/code_generator/typed_number.mli b/src/plugins/e-acsl/src/code_generator/typed_number.mli index 5be164a3d7c..6f56f8ed162 100644 --- a/src/plugins/e-acsl/src/code_generator/typed_number.mli +++ b/src/plugins/e-acsl/src/code_generator/typed_number.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Manipulate the type of numbers. *) diff --git a/src/plugins/e-acsl/src/dune b/src/plugins/e-acsl/src/dune index 50148161658..bf7f6dde4c7 100644 --- a/src/plugins/e-acsl/src/dune +++ b/src/plugins/e-acsl/src/dune @@ -17,6 +17,7 @@ ;; ;; ;; See the GNU Lesser General Public License version 2.1 ;; ;; for more details (enclosed in the file licenses/LGPLv2.1). ;; +;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (rule diff --git a/src/plugins/e-acsl/src/libraries/analyses_datatype.ml b/src/plugins/e-acsl/src/libraries/analyses_datatype.ml index 364f2b5e04d..e3d1f599319 100644 --- a/src/plugins/e-acsl/src/libraries/analyses_datatype.ml +++ b/src/plugins/e-acsl/src/libraries/analyses_datatype.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Datatypes for analyses types *) diff --git a/src/plugins/e-acsl/src/libraries/analyses_datatype.mli b/src/plugins/e-acsl/src/libraries/analyses_datatype.mli index d7ba09fdb73..444219dfc2f 100644 --- a/src/plugins/e-acsl/src/libraries/analyses_datatype.mli +++ b/src/plugins/e-acsl/src/libraries/analyses_datatype.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Datatypes for analyses types *) diff --git a/src/plugins/e-acsl/src/libraries/analyses_types.ml b/src/plugins/e-acsl/src/libraries/analyses_types.ml index c883892db32..7f644b2eb0b 100644 --- a/src/plugins/e-acsl/src/libraries/analyses_types.ml +++ b/src/plugins/e-acsl/src/libraries/analyses_types.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Types used by E-ACSL analyses *) diff --git a/src/plugins/e-acsl/src/libraries/builtins.ml b/src/plugins/e-acsl/src/libraries/builtins.ml index 6046e7ea5ce..e09d5b889a2 100644 --- a/src/plugins/e-acsl/src/libraries/builtins.ml +++ b/src/plugins/e-acsl/src/libraries/builtins.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/libraries/builtins.mli b/src/plugins/e-acsl/src/libraries/builtins.mli index 2c455a8b093..1e1f9451350 100644 --- a/src/plugins/e-acsl/src/libraries/builtins.mli +++ b/src/plugins/e-acsl/src/libraries/builtins.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** E-ACSL built-in database. *) diff --git a/src/plugins/e-acsl/src/libraries/error.ml b/src/plugins/e-acsl/src/libraries/error.ml index 4805a79f4d0..5cd7569f230 100644 --- a/src/plugins/e-acsl/src/libraries/error.ml +++ b/src/plugins/e-acsl/src/libraries/error.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Internal module holding the exception of [Error]. diff --git a/src/plugins/e-acsl/src/libraries/error.mli b/src/plugins/e-acsl/src/libraries/error.mli index d27568646e9..6eb07dc42c8 100644 --- a/src/plugins/e-acsl/src/libraries/error.mli +++ b/src/plugins/e-acsl/src/libraries/error.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Handling errors. *) diff --git a/src/plugins/e-acsl/src/libraries/functions.ml b/src/plugins/e-acsl/src/libraries/functions.ml index 3c119a46d54..2f8ee15c6fd 100644 --- a/src/plugins/e-acsl/src/libraries/functions.ml +++ b/src/plugins/e-acsl/src/libraries/functions.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/libraries/functions.mli b/src/plugins/e-acsl/src/libraries/functions.mli index 2ceecfb83c8..464024bc3be 100644 --- a/src/plugins/e-acsl/src/libraries/functions.mli +++ b/src/plugins/e-acsl/src/libraries/functions.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/libraries/gmp_types.ml b/src/plugins/e-acsl/src/libraries/gmp_types.ml index 9eb6aba9bce..78d2dee5f0e 100644 --- a/src/plugins/e-acsl/src/libraries/gmp_types.ml +++ b/src/plugins/e-acsl/src/libraries/gmp_types.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** GMP Values. *) diff --git a/src/plugins/e-acsl/src/libraries/gmp_types.mli b/src/plugins/e-acsl/src/libraries/gmp_types.mli index 50e70f37d46..73159d06de1 100644 --- a/src/plugins/e-acsl/src/libraries/gmp_types.mli +++ b/src/plugins/e-acsl/src/libraries/gmp_types.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** GMP Values. *) diff --git a/src/plugins/e-acsl/src/libraries/interval_utils.ml b/src/plugins/e-acsl/src/libraries/interval_utils.ml index 22071bef2f5..41c50a29fcb 100644 --- a/src/plugins/e-acsl/src/libraries/interval_utils.ml +++ b/src/plugins/e-acsl/src/libraries/interval_utils.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/libraries/interval_utils.mli b/src/plugins/e-acsl/src/libraries/interval_utils.mli index 55af526ae7a..90c57989716 100644 --- a/src/plugins/e-acsl/src/libraries/interval_utils.mli +++ b/src/plugins/e-acsl/src/libraries/interval_utils.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (* This module serves as a library for the modules Interval and Widening, the diff --git a/src/plugins/e-acsl/src/libraries/logic_aggr.ml b/src/plugins/e-acsl/src/libraries/logic_aggr.ml index 696c9d6c376..433a1a892de 100644 --- a/src/plugins/e-acsl/src/libraries/logic_aggr.ml +++ b/src/plugins/e-acsl/src/libraries/logic_aggr.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) type t = diff --git a/src/plugins/e-acsl/src/libraries/logic_aggr.mli b/src/plugins/e-acsl/src/libraries/logic_aggr.mli index b38313c42b3..4c01586e1eb 100644 --- a/src/plugins/e-acsl/src/libraries/logic_aggr.mli +++ b/src/plugins/e-acsl/src/libraries/logic_aggr.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml index 01ea9257274..839b26676fd 100644 --- a/src/plugins/e-acsl/src/libraries/misc.ml +++ b/src/plugins/e-acsl/src/libraries/misc.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli index 38fb89df7bd..16706184a7f 100644 --- a/src/plugins/e-acsl/src/libraries/misc.mli +++ b/src/plugins/e-acsl/src/libraries/misc.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Utilities for E-ACSL. *) diff --git a/src/plugins/e-acsl/src/libraries/varname.ml b/src/plugins/e-acsl/src/libraries/varname.ml index 47e43077c17..2a311b9dd72 100644 --- a/src/plugins/e-acsl/src/libraries/varname.ml +++ b/src/plugins/e-acsl/src/libraries/varname.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/libraries/varname.mli b/src/plugins/e-acsl/src/libraries/varname.mli index 244441ab490..4905dbb8871 100644 --- a/src/plugins/e-acsl/src/libraries/varname.mli +++ b/src/plugins/e-acsl/src/libraries/varname.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (* Variable name generator wrt a lexical scope. *) diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml index f351d6174a0..0d8043ee7fe 100644 --- a/src/plugins/e-acsl/src/main.ml +++ b/src/plugins/e-acsl/src/main.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) module Resulting_projects = diff --git a/src/plugins/e-acsl/src/main.mli b/src/plugins/e-acsl/src/main.mli index 6818e5996f6..ff9da6479e3 100644 --- a/src/plugins/e-acsl/src/main.mli +++ b/src/plugins/e-acsl/src/main.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Register the plugin in the Frama-C kernel. Nothing is exported. *) diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml index 342ccfcf432..506c123ac28 100644 --- a/src/plugins/e-acsl/src/options.ml +++ b/src/plugins/e-acsl/src/options.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) let () = Plugin.is_share_visible () diff --git a/src/plugins/e-acsl/src/options.mli b/src/plugins/e-acsl/src/options.mli index a3e633ad24f..295e66799a6 100644 --- a/src/plugins/e-acsl/src/options.mli +++ b/src/plugins/e-acsl/src/options.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) include Plugin.S (** implementation of Log.S for E-ACSL *) diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml index a4dc26b6a46..9e21ae9804e 100644 --- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml +++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli index 89326169cd4..8de126f92aa 100644 --- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli +++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** Prepare AST for E-ACSL generation. diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml index 169753377d5..be5d5eb32d2 100644 --- a/src/plugins/e-acsl/src/project_initializer/rtl.ml +++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) open Cil_types diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.mli b/src/plugins/e-acsl/src/project_initializer/rtl.mli index 1b2d5256639..4302f9cf37e 100644 --- a/src/plugins/e-acsl/src/project_initializer/rtl.mli +++ b/src/plugins/e-acsl/src/project_initializer/rtl.mli @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (** This module links the E-ACSL's RTL to the user source code. *) diff --git a/src/plugins/e-acsl/tab-in-changelog.sh b/src/plugins/e-acsl/tab-in-changelog.sh index 7be734713be..b2e31bc0b33 100755 --- a/src/plugins/e-acsl/tab-in-changelog.sh +++ b/src/plugins/e-acsl/tab-in-changelog.sh @@ -18,6 +18,7 @@ # # # See the GNU Lesser General Public License version 2.1 # # for more details (enclosed in the file licenses/LGPLv2.1). # +# # ########################################################################## # Base dir of this script diff --git a/src/plugins/e-acsl/tests/E_ACSL_test.ml b/src/plugins/e-acsl/tests/E_ACSL_test.ml index 5647bd1d79b..f91a556d5a4 100644 --- a/src/plugins/e-acsl/tests/E_ACSL_test.ml +++ b/src/plugins/e-acsl/tests/E_ACSL_test.ml @@ -17,6 +17,7 @@ (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) (**************************************************************************) (* return true if the global g has been generated by E-ACSL *) diff --git a/src/plugins/e-acsl/tests/wrapper.sh b/src/plugins/e-acsl/tests/wrapper.sh index fcf137e29a0..6e6805b564d 100755 --- a/src/plugins/e-acsl/tests/wrapper.sh +++ b/src/plugins/e-acsl/tests/wrapper.sh @@ -18,6 +18,7 @@ # # # See the GNU Lesser General Public License version 2.1 # # for more details (enclosed in the file licenses/LGPLv2.1). # +# # ########################################################################## # Wrapper script to compile a test file and execute the resulting binary diff --git a/tools/lint/UTF8.ml b/tools/lint/UTF8.ml index 92ec9c556fc..b91a0b05b2c 100644 --- a/tools/lint/UTF8.ml +++ b/tools/lint/UTF8.ml @@ -38,6 +38,7 @@ (* *) (* File modified by CEA (Commissariat à l'énergie atomique et aux *) (* énergies alternatives). *) +(* *) (***************************************************************************) (* Function extracted from Camomile library and modified by CEA to get the -- GitLab