diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-10 15:01:03 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-10 15:01:03 +0200 |
| commit | 28108aeb3b0fd9ffbb449715b9b0cd8599fb0027 (patch) | |
| tree | d6892a4f59f7ef71f5e8cfea00d159eddd7d0bac /aarch64/Asmblock.v | |
| parent | 3795aaf024d8585a6050ca16c4ea634dcb1f36cd (diff) | |
| download | compcert-kvx-28108aeb3b0fd9ffbb449715b9b0cd8599fb0027.tar.gz compcert-kvx-28108aeb3b0fd9ffbb449715b9b0cd8599fb0027.zip | |
fix size of block in Asmblock
Due to the fact that, at the Asm level, Plabel runs PC++
Diffstat (limited to 'aarch64/Asmblock.v')
| -rw-r--r-- | aarch64/Asmblock.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 74956bcd..e362753b 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -505,14 +505,11 @@ Definition length_opt {A} (o: option A) : nat := | None => 0 end. -(* WARNING: the notion of size is not the same than in Machblock ! - We ignore labels here... - - This notion of size induces the notion of "valid" code address given by [find_bblock] +(* This notion of size induces the notion of "valid" code address given by [find_bblock] The result is in Z to be compatible with operations on PC. *) -Definition size (b:bblock): Z := Z.of_nat (length (body b) + length_opt (exit b)). +Definition size (b:bblock): Z := Z.of_nat (length (header b) + length (body b) + length_opt (exit b)). Definition bblocks := list bblock. |