diff options
| -rw-r--r-- | aarch64/Asmblock.v | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 193941aa..2d0eeb11 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -1229,14 +1229,16 @@ Definition arith_eval_p (i : arith_p) : val := | Pfmovimmd f => Vfloat f end. +Definition if_opt_bool_val (c: option bool) v1 v2: val := + match c with + | Some true => v1 + | Some false => v2 + | None => Vundef + end. + Definition arith_eval_c_p (i : arith_c_p) (c : option bool) : val := match i with - | Pcset => - (match c with - | Some true => Vint Int.one - | Some false => Vint Int.zero - | None => Vundef - end) + | Pcset => if_opt_bool_val c (Vint Int.one) (Vint Int.zero) end. Definition arith_eval_pp i v := @@ -1311,8 +1313,10 @@ Definition arith_eval_ppp i v1 v2 := end. Definition arith_eval_c_ppp (i : arith_c_ppp) (v1 v2 : val) (c : option bool) := + if_opt_bool_val c v1 v2. + (* match i with - | Pcsel => + | Pcsel => (match c with | Some true => v1 | Some false => v2 @@ -1325,6 +1329,7 @@ Definition arith_eval_c_ppp (i : arith_c_ppp) (v1 v2 : val) (c : option bool) := | None => Vundef end) end. + *) Definition arith_rr0r_isize (i: arith_rr0r) := match i with |