Skip to content
Snippets Groups Projects
Commit 6f8e435d authored by Patrick Baudin's avatar Patrick Baudin
Browse files

Merge branch 'feature/patrick/eacl-fixes-c-indentation' into 'master'

[E-ACSL] fixes c indentation

See merge request frama-c/frama-c!3814
parents 35afda71 f42b4831
No related branches found
No related tags found
No related merge requests found
...@@ -36,3 +36,4 @@ aef808e15e4dcc02dcee7004add8530083d33474 ...@@ -36,3 +36,4 @@ aef808e15e4dcc02dcee7004add8530083d33474
220072cecdcc0b0b8292c40d93e793b3219b506f 220072cecdcc0b0b8292c40d93e793b3219b506f
6ead6d862f1960e6baca64d335b811c954cf8430 6ead6d862f1960e6baca64d335b811c954cf8430
7955ef2039b2010cc30b88da7a47d4f07e298042 7955ef2039b2010cc30b88da7a47d4f07e298042
8353ff71c9958169cf27c589b678f183cca63a9c
...@@ -2,6 +2,9 @@ ...@@ -2,6 +2,9 @@
# HEADER_SPEC: CEA_LGPL_OR_PROPRIETARY.E_ACSL # # 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 configure.ac header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
Makefile 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 ...@@ -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
/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 # # HEADER_SPEC: .ignore #
######################## ########################
...@@ -60,10 +70,9 @@ README header_spec=.ignore ...@@ -60,10 +70,9 @@ README header_spec=.ignore
/tests/test_config header_spec=.ignore /tests/test_config header_spec=.ignore
/tests/test_config_dev 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/wrapper.sh header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
/tests/E_ACSL_test.ml 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 /contrib/libdlmalloc/dlmalloc.* header_spec=MODIFIED_DLMALLOC
/share/e-acsl/internals/e_acsl_rtl_io.* header_spec=MODIFIED_SPARETIMELABS /share/e-acsl/internals/e_acsl_rtl_io.* header_spec=MODIFIED_SPARETIMELABS
...@@ -167,7 +167,7 @@ void validate_shadow_layout() { ...@@ -167,7 +167,7 @@ void validate_shadow_layout() {
# endif # endif
/* Each segment has 3 partitions: /* Each segment has 3 partitions:
- application memory - application memory
- primary/secondary shadows */ - primary/secondary shadows */
int num_partitions = sizeof(mem_partitions) / sizeof(memory_partition *); int num_partitions = sizeof(mem_partitions) / sizeof(memory_partition *);
int num_seg_in_part = 3; int num_seg_in_part = 3;
......
/* run.config /* 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. function in the presence of early return.
*/ */
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment