diff options
| author | Brian Campbell | 2018-09-05 14:06:58 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-09-05 14:26:17 +0100 |
| commit | d27c1dcae22d624e0ba8ec5c6790b1466fb2a3e3 (patch) | |
| tree | 79bed32c1741867196284976681aaa0e07ef883f /riscv | |
| parent | 5ade6d23451173788ab9283127d4ec7d1e8fb761 (diff) | |
Coq: fill in trivial ranges in constraint solver
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/coq.patch | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/riscv/coq.patch b/riscv/coq.patch index 983b7ac1..17398e36 100644 --- a/riscv/coq.patch +++ b/riscv/coq.patch @@ -78,26 +78,6 @@ (match w__7 with | PTW_Failure (f) => returnm ((TR39_Failure (f)) : TR39_Result ) | PTW_Success (pAddr,pte,pteAddr,(existT _ level _),global) => -@@ -8681,7 +8683,7 @@ - | Sbare => returnm ((TR_Address (vAddr)) : TR_Result ) - | SV39 => - translate39 (subrange_vec_dec vAddr 38 0) ac effPriv mxr do_sum -- (build_ex (projT1 (sub_range (build_ex SV39_LEVELS) (build_ex 1)))) >>= fun w__7 : TR39_Result => -+ (build_ex ( (Z.sub ( SV39_LEVELS) ( 1)))) >>= fun w__7 : TR39_Result => - returnm ((match w__7 with - | TR39_Address (pa) => TR_Address (EXTZ 64 pa) - | TR39_Failure (f) => TR_Failure (translationException ac f) -@@ -12178,8 +12180,8 @@ - if sumbool_of_bool ((andb s - (Z.gtb q (projT1 (sub_range (build_ex (projT1 (pow2 31))) (build_ex 1)))))) - then -- projT1 (sub_range (build_ex 0) -- (build_ex (projT1 ((build_ex (projT1 (ex_int (pow 2 31)))) -+ (Z.sub ( 0) -+ ( (projT1 ((build_ex (projT1 (ex_int (pow 2 31)))) - : {n : Z & ArithFact (True)})))) - else q in - wX @@ -12374,138 +12376,144 @@ returnm (true : bool). |