diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs index eb5ae4704b269753011df720e74d521d6a0b352d..3101a85521c753f082694f2bc35ba9c81e42abaf 100644 --- a/.git-blame-ignore-revs +++ b/.git-blame-ignore-revs @@ -36,3 +36,4 @@ aef808e15e4dcc02dcee7004add8530083d33474 220072cecdcc0b0b8292c40d93e793b3219b506f 6ead6d862f1960e6baca64d335b811c954cf8430 7955ef2039b2010cc30b88da7a47d4f07e298042 +8353ff71c9958169cf27c589b678f183cca63a9c diff --git a/src/plugins/e-acsl/.gitattributes b/src/plugins/e-acsl/.gitattributes index cca30ad415b5e0fc3ed4672497b187c825f437bf..9d7633a570624354415012aa73ba25e820304174 100644 --- a/src/plugins/e-acsl/.gitattributes +++ b/src/plugins/e-acsl/.gitattributes @@ -2,6 +2,9 @@ # HEADER_SPEC: CEA_LGPL_OR_PROPRIETARY.E_ACSL # ############################################### +dune-project header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL +dune header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL + configure.ac header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL Makefile header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL @@ -20,6 +23,13 @@ Makefile.in header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL /scripts/e-acsl-gcc.sh.comp header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL /scripts/e-acsl-gcc.sh.comp header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL +########################################### +# CHECK-INDENT # +########################################### + +/tests/*/*.c check-syntax check-indent +/share/**/*.c check-syntax check-indent + ######################## # HEADER_SPEC: .ignore # ######################## @@ -60,10 +70,9 @@ README header_spec=.ignore /tests/test_config header_spec=.ignore /tests/test_config_dev header_spec=.ignore -/tests/**/* header_spec +/tests/**/* header_spec=.ignore /tests/wrapper.sh header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL /tests/E_ACSL_test.ml header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL /contrib/libdlmalloc/dlmalloc.* header_spec=MODIFIED_DLMALLOC /share/e-acsl/internals/e_acsl_rtl_io.* header_spec=MODIFIED_SPARETIMELABS - 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 608c3bf745430f67205aadd40206e6f869dace2a..2bf9f0f91ec839b315f2dc47b30fc45f14e41519 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 @@ -167,7 +167,7 @@ void validate_shadow_layout() { # endif /* Each segment has 3 partitions: - - application memory + - application memory - primary/secondary shadows */ int num_partitions = sizeof(mem_partitions) / sizeof(memory_partition *); int num_seg_in_part = 3; diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-105.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-105.c index 3878a97a1d6a1b319cf5893a152b6d3b65d85b7e..d8a64368f3045c94265d674bcbc21036a24d6192 100644 --- a/src/plugins/e-acsl/tests/bts/issue-eacsl-105.c +++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-105.c @@ -1,5 +1,5 @@ /* run.config - COMMENT: frama-c/e-acsl#105, test for delete block before exiting the + COMMENT: frama-c/e-acsl#105, test for delete block before exiting the function in the presence of early return. */