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..9e5dd8f5f57cc7ae8befa78281fae1ec6a13849a 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. */