diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-29 16:59:31 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-29 16:59:31 +0100 |
| commit | 7e59d2723fb9c5b4631f5eac1e99ae8956871a7f (patch) | |
| tree | d45156795947e1aaf95e0dfa4a0c7f76b3a1fb85 /src/translation/HTLgen.v | |
| parent | f57793552fe387fef22f6a77389de2556c0354a4 (diff) | |
| download | vericert-kvx-7e59d2723fb9c5b4631f5eac1e99ae8956871a7f.tar.gz vericert-kvx-7e59d2723fb9c5b4631f5eac1e99ae8956871a7f.zip | |
Develop compiles again
Diffstat (limited to 'src/translation/HTLgen.v')
| -rw-r--r-- | src/translation/HTLgen.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 59fb70a..b32ed9d 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -294,24 +294,24 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon ex | Op.Aindexed off, r1::nil => if (check_address_parameter_signed off) then ret (boplitz Vadd r1 off) - else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address misaligned") | Op.Ascaled scale offset, r1::nil => if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) - else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address misaligned") | Op.Aindexed2 offset, r1::r2::nil => if (check_address_parameter_signed offset) then ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 offset)) - else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address misaligned") | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) then ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) - else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address misaligned") | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in if (check_address_parameter_unsigned a) then ret (Vlit (ZToValue 32 a)) - else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address misaligned") | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") end. |