extraction de max_sum -> joli petit bug d'extraction a corriger !

doc/exec.tex

@@ -59,9 +59,11 @@ among which we find a file \texttt{maxsum\_\_MaxAndSum.ml} containing
 the OCaml code for functions \texttt{max\_sum} and \texttt{test}.
 
 To compile it, we create a file \texttt{main.ml}
-containing a call to \texttt{test}, that is
+containing a call to \texttt{test}, that is for example
 \begin{whycode}
-  let () = test ()
+  let (s,m) = test () in
+  Format.printf "sum=%s, max=%s@." 
+    (Why3__BigInt.to_string s) (Why3__BigInt.to_string m)
 \end{whycode}
 and we pass both files \texttt{maxsum\_\_MaxAndSum.ml} and
 \texttt{main.ml} to the OCaml compiler:

examples/vstte10_max_sum.mlw

@@ -60,7 +60,7 @@ module TestCase
 
   exception BenchFailure
 
-  let test_case () raises { BenchFailure -> true } =
+  let test () =
     let n = 10 in
     let a = make n 0 in
     a[0] <- 9;
@@ -73,7 +73,10 @@ module TestCase
     a[7] <- 1;
     a[8] <- 10;
     a[9] <- 6;
-    let (s, m) = max_sum a n in
+    max_sum a n
+
+  let test_case () raises { BenchFailure -> true } =
+    let (s, m) = test () in
     assert { s = 45 };
     assert { m = 10 };
     (* bench of --exec *)

examples/vstte10_max_sum/Makefile.in

+
+MAIN=main
+OBJ=vstte10_max_sum__MaxAndSum2 vstte10_max_sum__TestCase
+
+ML  = $(addsuffix .ml, $(OBJ))
+CMO = $(addsuffix .cmo, $(OBJ))
+CMX = $(addsuffix .cmx, $(OBJ))
+
+OCAMLOPT=ocamlopt -noassert -inline 1000
+
+INCLUDE=@BIGINTINCLUDE@ -I ../../lib/why3
+
+all: $(MAIN).@OCAMLBEST@
+
+extract: $(ML)
+
+$(MAIN).byte: $(CMO)  $(MAIN).cmo
+	ocamlc $(INCLUDE) @BIGINTLIB@.cma why3extract.cma -o $@ $^
+
+$(MAIN).opt: $(CMX)  $(MAIN).cmx
+	$(OCAMLOPT) $(INCLUDE) @BIGINTLIB@.cmxa why3extract.cmxa -o $@ $^
+
+$(MAIN).cmx: $(CMX)
+
+$(ML): ../vstte10_max_sum.mlw
+	../../bin/why3 -E ocaml32 ../vstte10_max_sum.mlw -o .
+
+%.cmx: %.ml
+	$(OCAMLOPT) $(INCLUDE) -annot -c $<
+
+%.cmo: %.ml
+	ocamlc $(INCLUDE) -annot -c $<
+
+%.cmi: %.mli
+	ocamlc $(INCLUDE) -annot -c $<
+
+clean::
+	rm -f $(ML) *.cm[xio] *.o *.annot $(MAIN).opt $(MAIN).byte
+	rm -f why3__*.ml* vstte10_max_sum__*.ml* int__*.ml*
+
+Makefile: Makefile.in ../../config.status
+	cd ../.. ; ./config.status chmod --file examples/vstte10_max_sum/Makefile
+
+

examples/vstte10_max_sum/main.ml

+
+open Why3extract
+open Format
+
+let () =
+  let (s,m) = Vstte10_max_sum__TestCase.test () in
+  printf "sum=%s, max=%s@."
+    (Why3__BigInt.to_string s) (Why3__BigInt.to_string m)