diff options
| author | James Pollard <james@pollard.dev> | 2020-07-07 13:24:59 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-07-07 13:24:59 +0100 |
| commit | b3208d9a581e7575c41d545964f4f85c6f3b4d66 (patch) | |
| tree | 1257ce97072eb80001ec05ee3ff8c330495c51ab /src/translation/HTLgen.v | |
| parent | 5baa025e8d26b91ac99f983bce44af5025e20b14 (diff) | |
| download | vericert-kvx-b3208d9a581e7575c41d545964f4f85c6f3b4d66.tar.gz vericert-kvx-b3208d9a581e7575c41d545964f4f85c6f3b4d66.zip | |
Get Coqup compiling again on dev-nadesh.
Diffstat (limited to 'src/translation/HTLgen.v')
| -rw-r--r-- | src/translation/HTLgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 32b6e04..babbc01 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -275,8 +275,8 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr : | Op.Ccompu c, _ => translate_comparison c args | Op.Ccompimm c i, _ => translate_comparison_imm c args i | Op.Ccompuimm c i, _ => translate_comparison_imm c args i - | Op.Cmaskzero n, r::nil => ret (Vbinop Veq (boplit Vand r n) (Vlit (ZToValue 32 0))) - | Op.Cmasknotzero n, r::nil => ret (Vbinop Vne (boplit Vand r n) (Vlit (ZToValue 32 0))) + | Op.Cmaskzero n, r::nil => ret (Vbinop Veq (boplit Vand r n) (Vlit (ZToValue 0))) + | Op.Cmasknotzero n, r::nil => ret (Vbinop Vne (boplit Vand r n) (Vlit (ZToValue 0))) | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other") end. |