diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-06 14:56:52 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-06 15:58:38 +0200 |
| commit | a7031d640f0f80ec1823b00b5cdf2b84303d3de7 (patch) | |
| tree | 8c5ff7dc970d98bb6e5757abd186a0700353faef /aarch64/Asmblock.v | |
| parent | 37cae55dfec69476155f3bb24a94d67ace594ba5 (diff) | |
| download | compcert-kvx-a7031d640f0f80ec1823b00b5cdf2b84303d3de7.tar.gz compcert-kvx-a7031d640f0f80ec1823b00b5cdf2b84303d3de7.zip | |
aarch64/Asmblock: Switch arith_c_r to arith_c_p for consistency
Diffstat (limited to 'aarch64/Asmblock.v')
| -rw-r--r-- | aarch64/Asmblock.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 7949632c..40219c5d 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -288,7 +288,7 @@ Inductive arith_p : Type := (* Arithmetic instructions with conditional execution *) (* TODO matching case in ar_instruction *) -Inductive arith_c_r : Type := +Inductive arith_c_p : Type := (** Conditional data processing *) | Pcset (**r set to 1/0 if cond is true/false *) (* @@ -526,7 +526,7 @@ Inductive arith_aaffff : Type := *) Inductive ar_instruction : Type := | PArithP (i : arith_p) (rd : preg) - | PArithCR (i : arith_c_r) (rd : ireg) (c : testcond) + | PArithCP (i : arith_c_p) (rd : preg) (c : testcond) | PArithRR (i : arith_rr) (rd rs : ireg) | PArithRF (i : arith_rf) (rd : ireg) (rs : freg) | PArithRRR (i : arith_rrr) (rd r1 r2 : ireg) @@ -1298,7 +1298,7 @@ Definition arith_eval_p (i : arith_p) : val := | Pmovk X pos => insert_in_long rs#rd n pos 16 *) end. -Definition arith_eval_c_r (i : arith_c_r) (c : option bool) : val := +Definition arith_eval_c_p (i : arith_c_p) (c : option bool) : val := match i with | Pcset => (match c with @@ -1542,7 +1542,7 @@ Definition arith_prepare_comparison_ff i (v1 v2 : val) := Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := match ai with | PArithP i d => rs#d <- (arith_eval_p i) - | PArithCR i d c => rs#d <- (arith_eval_c_r i (eval_testcond c rs)) + | PArithCP i d c => rs#d <- (arith_eval_c_p i (eval_testcond c rs)) | PArithRR i d s => rs#d <- (arith_eval_rr i rs#s) | PArithRF i d s => rs#d <- (arith_eval_rf i rs#s) | PArithRRR i d s1 s2 => rs#d <- (arith_eval_rrr i rs#s1 rs#s2) |