diff options
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. |