CN: Fix and re-enable formatting

c77d645 accidentally deleted the formatting CI check and d7b47b7 committed badly formatted code. This commit fixes both of the above.
rems-project · Jul 30, 2024 · 29e8f7c · 29e8f7c
1 parent fa710e6
commit 29e8f7c
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 15 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -126,6 +126,7 @@ jobs:
       run: |
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
+        USE_OPAM='' cd backend/cn && dune build @fmt
 
     - name: Install Cerberus-CHERI
       if: ${{ matrix.version == '4.14.1' }}

diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml
@@ -559,21 +559,21 @@ let rec check_pexpr (pe : BT.t mu_pexpr) (k : IT.t -> unit m) : unit m =
                 let@ model = model () in
                 let ub = CF.Undefined.UB045a_division_by_zero in
                 fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } })))
-          | OpRem_t ->
-             let@ () = WellTyped.ensure_base_type loc ~expect (bt_of_pexpr pe1) in
-             let@ () = WellTyped.ensure_bits_type loc expect in
-             let@ () = WellTyped.ensure_bits_type loc (bt_of_pexpr pe2) in
-             check_pexpr pe1 (fun v1 ->
-              check_pexpr pe2 (fun v2 ->
-                let@ provable = provable loc in
-                let v2_bt = bt_of_pexpr pe2 in
-                let here = Locations.other __FUNCTION__ in
-                match provable (t_ (ne_ (v2, int_lit_ 0 v2_bt here) here)) with
-                | `True -> k (rem_ (v1, v2) loc)
-                | `False -> 
-                  let@ model = model () in
-                  let ub = CF.Undefined.UB045b_modulo_by_zero in
-                  fail (fun ctxt -> {loc; msg = Undefined_behaviour {ub; ctxt; model}})))
+        | OpRem_t ->
+          let@ () = WellTyped.ensure_base_type loc ~expect (bt_of_pexpr pe1) in
+          let@ () = WellTyped.ensure_bits_type loc expect in
+          let@ () = WellTyped.ensure_bits_type loc (bt_of_pexpr pe2) in
+          check_pexpr pe1 (fun v1 ->
+            check_pexpr pe2 (fun v2 ->
+              let@ provable = provable loc in
+              let v2_bt = bt_of_pexpr pe2 in
+              let here = Locations.other __FUNCTION__ in
+              match provable (t_ (ne_ (v2, int_lit_ 0 v2_bt here) here)) with
+              | `True -> k (rem_ (v1, v2) loc)
+              | `False ->
+                let@ model = model () in
+                let ub = CF.Undefined.UB045b_modulo_by_zero in
+                fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } })))
         | OpEq ->
           let@ () = WellTyped.ensure_base_type loc ~expect Bool in
           let@ () =