Fixes redundant os constraints and add more CI

.github/workflows/build.yml

@@ -20,6 +20,8 @@ jobs:
           - "4.14"
           - "5.1"
     runs-on: ${{ matrix.os }}
+    env:
+      OPAMCONFIRMLEVEL: unsafe-yes # allow opam depext to yes package manager prompts
     steps:
       - name: Checkout
         uses: actions/checkout@v4

.github/workflows/lower-bounds.yml

@@ -0,0 +1,46 @@
+# Credit for this workflow:
+# https://sim642.eu/blog/2022/03/13/ocaml-dependencies-lower-bounds-ci/
+name: Lower bounds
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+jobs:
+  lower-bounds:
+    fail-fast: false
+    strategy:
+      matrix:
+        os:
+          - ubuntu-latest
+          - macos-latest
+        ocaml-compiler:
+          - "4.14"
+          - "5.1"
+    runs-on: ${{ matrix.os }}
+    env:
+      OPAMCONFIRMLEVEL: unsafe-yes # allow opam depext to yes package manager prompts
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+      - name: Set up OCaml ${{ matrix.ocaml-compiler }}
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          dune-cache: true
+          allow-prerelease-opam: true
+      - name: Install dependencies
+        run: opam install . --deps-only --with-test
+      - name: Install opam-0install
+        run: opam install opam-0install
+      - name: Downgrade dependencies
+        run: opam install --unlock-base $(opam exec -- opam-0install --prefer-oldest --with-test smtml)
+      - name: Build
+        run: opam exec -- dune build @install
+      - name: Test
+        run: opam exec -- dune runtest
+

lib/eval.ml

@@ -286,15 +286,21 @@ module I32 = struct
     Int32.logor (shr_u x (Int32.of_int n)) (shl x (Int32.of_int (32 - n)))
   [@@inline]
 
+  let clz n =
+    let n = Ocaml_intrinsics.Int32.count_leading_zeros n in
+    Int32.of_int n
+
+  let ctz n =
+    let n = Ocaml_intrinsics.Int32.count_trailing_zeros n in
+    Int32.of_int n
+
   let unop (op : unop) (v : Value.t) : Value.t =
     let f =
       match op with
       | Neg -> Int32.neg
       | Not -> Int32.lognot
-      | Clz ->
-        fun n -> Int32.of_int (Ocaml_intrinsics.Int32.count_leading_zeros n)
-      | Ctz ->
-        fun n -> Int32.of_int (Ocaml_intrinsics.Int32.count_trailing_zeros n)
+      | Clz -> clz
+      | Ctz -> ctz
       | _ -> Log.err {|unop: Unsupported i32 operator "%a"|} Ty.pp_unop op
     in
     to_value (f (of_value 1 v))
@@ -379,15 +385,21 @@ module I64 = struct
     Int64.logor (shr_u x (Int64.of_int n)) (shl x (Int64.of_int (64 - n)))
   [@@inline]
 
+  let clz n =
+    let n = Ocaml_intrinsics.Int64.count_leading_zeros n in
+    Int64.of_int n
+
+  let ctz n =
+    let n = Ocaml_intrinsics.Int64.count_trailing_zeros n in
+    Int64.of_int n
+
   let unop (op : unop) (v : Value.t) : Value.t =
     let f =
       match op with
       | Neg -> Int64.neg
       | Not -> Int64.lognot
-      | Clz ->
-        fun n -> Int64.of_int (Ocaml_intrinsics.Int64.count_leading_zeros n)
-      | Ctz ->
-        fun n -> Int64.of_int (Ocaml_intrinsics.Int64.count_trailing_zeros n)
+      | Clz -> clz
+      | Ctz -> ctz
       | _ -> Log.err {|unop: Unsupported i64 operator "%a"|} Ty.pp_unop op
     in
     to_value (f (of_value 1 v))

smtml.opam

@@ -39,3 +39,8 @@ build: [
   ]
 ]
 dev-repo: "git+https://github.com/formalsec/smtml.git"
+available: arch != "arm32" & arch != "x86_32"
+pin-depends: [
+  ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#ae18d699b19e7967a81ccae6db454edfa968feae"]
+  ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#ae18d699b19e7967a81ccae6db454edfa968feae"]
+]

smtml.opam.template

@@ -0,0 +1,5 @@
+available: arch != "arm32" & arch != "x86_32"
+pin-depends: [
+  ["colibri2.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#ae18d699b19e7967a81ccae6db454edfa968feae"]
+  ["colibrilib.0.4.0" "git+https://git.frama-c.com/pub/colibrics.git#ae18d699b19e7967a81ccae6db454edfa968feae"]
+]