check extraction in bench

.gitignore

@@ -190,6 +190,8 @@ pvsbin/
 /examples/why3bench.html
 /examples/why3regtests.err
 /examples/why3regtests.out
+/examples/*/*.ml
+/examples/*/*.opt
 /examples/*/*.html
 /examples/*/*/*.html
 /examples/*/*/*/*.html

Makefile.in

@@ -1210,7 +1210,7 @@ byte: $(OCAMLLIBS_CMO)
 
 install_no_local::
 	mkdir -p $(LIBDIR)/why3/ocaml
-	cp lib/ocaml/*.cm[iox] $(LIBDIR)/why3/ocaml
+	cp lib/ocaml/*.cm[iox] lib/ocaml/*.o $(LIBDIR)/why3/ocaml
 
 install_local: bin/why3doc
 

bench/bench

@@ -78,6 +78,25 @@ execute () {
     fi
 }
 
+extract_and_run () {
+    echo -n "$1... "
+    if make -C $1 > /dev/null 2>&1; then
+       if $1/main.opt $2 > /dev/null 2>&1; then
+           echo "ok"
+       else
+           echo "execution failed!"
+           echo $1/main.opt $2
+           $1/main.opt $2
+           exit 1
+       fi
+    else
+        echo "extract or compilation failed!"
+        echo make -C $1
+        make -C $1
+        exit 1
+    fi
+}
+
 list_stuff () {
     echo -n "$1 "
     if $pgm $1 > /dev/null 2>&1; then
@@ -153,6 +172,10 @@ execute examples/vstte10_queens.mlw NQueens.test8
 # examples/in_progress/residual.mlw --exec Test.test_astar
 echo ""
 
+echo "=== Extraction to Ocaml ==="
+extract_and_run examples/euler001 1000000
+echo ""
+
 echo "=== Checking drivers ==="
 drivers drivers
 echo ""

examples/euler001/Makefile

+
+OBJS=euler001__Euler001.cmx main.cmx
+
+NAME=main
+
+OCAMLOPT=ocamlopt -noassert -inline 100
+
+$(NAME).opt: $(OBJS)
+	$(OCAMLOPT) -I /usr/local/lib/why3/ocaml \
+	nums.cmxa why3__BuiltIn.cmx int__Int.cmx int__ComputerDivision.cmx \
+	-o $@ $^
+
+main.cmx: euler001__Euler001.cmx
+
+euler001__Euler001.ml: ../euler001.mlw
+	why3 -E ocaml ../euler001.mlw -o .
+
+%.cmx: %.ml 
+	ocamlopt -I /usr/local/lib/why3/ocaml -annot -c $<
+
+%.cmo: %.ml 
+	ocamlc -I /usr/local/lib/why3/ocaml -annot -c $<
+
+%.cmi: %.mli 
+	ocamlc -I /usr/local/lib/why3/ocaml -annot -c $<
+
+clean::
+	rm -f *.cm[xio] $(NAME).opt
+

examples/euler001/main.ml

+
+open Format
+
+let usage () =
+  eprintf "Euler001: sum of all the multiples of 3 or 5 below a given number@.";
+  eprintf "Usage: %s <decimal number>@." Sys.argv.(0);
+  exit 2
+
+let input =
+  if Array.length Sys.argv <> 2 then usage ();
+  Sys.argv.(1)
+
+let input_num =
+  try
+    Why3__BuiltIn.int_constant input
+  with _ -> usage ()
+
+let () =
+  let a = Euler001__Euler001.solve input_num in
+  printf "The sum of all the multiples of 3 or 5 below %s is %s@." 
+    (Num.string_of_num input_num) (Num.string_of_num a)