Error when using the ocaml-unsafe-int extraction driver
I'm trying to use the ocaml-unsafe-int
extraction driver on a simple example program (the maxsum code from the manual).
With the ocaml64 driver extraction it works:
$ why3 extract -D ocaml64 maxsum.mlw -o max_sum.ml # ok
but if I try to use ocaml-unsafe-int
instead, I get an error:
$ why3 extract -D ocaml-unsafe-int maxsum.mlw -o max_sum.ml
`syntax predicate' is invalid in extraction drivers, use `syntax val' instead.
For completeness, maxsum.mlw
contains:
module MaxAndSum
use int.Int
use ref.Ref
use array.Array
let max_sum (a: array int) (n: int) : (int, int)
requires { n = length a }
requires { forall i. 0 <= i < n -> a[i] >= 0 }
returns { sum, max -> sum <= n * max }
= let sum = ref 0 in
let max = ref 0 in
for i = 0 to n - 1 do
invariant { !sum <= i * !max }
if !max < a[i] then max := a[i];
sum := !sum + a[i]
done;
!sum, !max
end