change default optimization level to O3

OCamlPro · Jul 4, 2024 · 3d3c7f9 · 3d3c7f9
1 parent 59e2e00
commit 3d3c7f9
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 6 deletions.
diff --git a/example/c/README.md b/example/c/README.md
@@ -257,8 +257,9 @@ int main() {
 }
 ```
 
+<!-- TODO: remove `-O1` once symbolic popcnt is implemented -->
 ```sh
-$ owi c ./dobble.c -w1 --no-value
+$ owi c -O1 ./dobble.c -w1 --no-value
 ...
 Model:
   (model
@@ -311,7 +312,7 @@ OPTIONS
        -o VAL, --output=VAL (absent=owi-out)
            write results to dir
 
-       -O VAL (absent=0)
+       -O VAL (absent=3)
            specify which optimization level to use
 
        --optimize

diff --git a/src/bin/owi.ml b/src/bin/owi.ml
@@ -117,7 +117,7 @@ let c_cmd =
   in
   let opt_lvl =
     let doc = "specify which optimization level to use" in
-    Arg.(value & opt string "0" & info [ "O" ] ~doc)
+    Arg.(value & opt string "3" & info [ "O" ] ~doc)
   in
   let testcomp =
     let doc = "test-comp mode" in

diff --git a/test/c/collections-c/pqueue_tests.t b/test/c/collections-c/pqueue_tests.t
@@ -1,5 +1,5 @@
 Pqueue tests:
-  $ owi c -I files/normal/include files/normal/src/pqueue.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/pqueue/pqueue_test_enqueue.c --no-value
+  $ owi c -O0 -I files/normal/include files/normal/src/pqueue.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/pqueue/pqueue_test_enqueue.c --no-value
   Trap: memory heap buffer overflow
   Model:
     (model
@@ -11,7 +11,7 @@ Pqueue tests:
       (symbol_5 i32))
   Reached problem!
   [13]
-  $ owi c -I files/normal/include files/normal/src/pqueue.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/pqueue/pqueue_test_pop.c --no-value
+  $ owi c -O0 -I files/normal/include files/normal/src/pqueue.c files/normal/src/common.c files/normal/src/utils.c files/normal/testsuite/pqueue/pqueue_test_pop.c --no-value
   Trap: memory heap buffer overflow
   Model:
     (model

diff --git a/test/c/test-comp/simple.t b/test/c/test-comp/simple.t
@@ -1,4 +1,4 @@
-  $ owi c --testcomp ./simple.c
+  $ owi c -O0 --testcomp ./simple.c
   Assert failure: (bool.ne (i32.mul symbol_0 symbol_0) (i32 0))
   Model:
     (model