Commit 2fc09908 authored by Basile Desloges 's avatar Basile Desloges
Browse files

Merge branch 'feature/basile/eacsl-segment-end-address' into 'master'

[eacsl] Fix address of end segment in RTL layout

See merge request frama-c/frama-c!2979
parents c4d10fb9 54ae5e5e
......@@ -25,6 +25,8 @@
Plugin E-ACSL <next-release>
############################
-* runtime [2021-03-30] Fix the end address of the memory segments in the
RTL layouts.
- E-ACSL [2021-03-25] Add support for `check` and `admit` annotations
(frama-c/e-acsl#142).
-* E-ACSL [2021-03-25] Fix wrong computation of the base pointer when
......
......@@ -427,7 +427,7 @@ void set_application_segment(memory_segment *seg, uintptr_t start,
seg->name = name;
seg->start = start;
seg->size = size;
seg->end = seg->start + seg->size;
seg->end = seg->start + seg->size - 1;
seg->mspace = msp;
seg->parent = NULL;
seg->shadow_ratio = 0;
......@@ -442,7 +442,7 @@ void set_shadow_segment(memory_segment *seg, memory_segment *parent,
seg->size = parent->size/seg->shadow_ratio;
seg->mspace = eacsl_create_mspace(seg->size + SHADOW_SEGMENT_PADDING, 0);
seg->start = (uintptr_t)eacsl_mspace_malloc(seg->mspace,1);
seg->end = seg->start + seg->size;
seg->end = seg->start + seg->size - 1;
seg->shadow_offset = parent->start - seg->start;
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment