From 8353ff71c9958169cf27c589b678f183cca63a9c Mon Sep 17 00:00:00 2001 From: Patrick Baudin <patrick.baudin@cea.fr> Date: Fri, 17 Jun 2022 17:55:37 +0200 Subject: [PATCH] [E-ACSL] linting 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..2bf9f0f91ec 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