From 3a22f8d00c93a0c2e4085c62f77b07204ab8b531 Mon Sep 17 00:00:00 2001 From: Allan Blanchard <allan.blanchard@cea.fr> Date: Wed, 15 Jun 2022 16:31:58 +0200 Subject: [PATCH] [e-acsl] fix syntax on some C files --- .../observation_model/segment_model/e_acsl_segment_tracking.c | 2 +- src/plugins/e-acsl/tests/bts/issue-eacsl-105.c | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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 608c3bf7454..9e5dd8f5f57 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 3878a97a1d6..d8a64368f30 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. */ -- GitLab