Hi,
with Félix Breton (in cc) we get the following behaviour:
module Bug
open FStar.HyperStack.IO
module I32 = FStar.Int32
let main () =
if (I32.((-1l) <^ 0l)) then print_string "correct\n" else print_string
"wrong\n";
0
This prints "wrong", and was compiled with:
bug-ocaml: out Bug.fst
$(FSTAR) $(FSTAR_DEFAULT_ARGS) --lax --odir out --codegen OCaml Bug.fst
echo "let _ = main ()" >> out/Bug.ml
$(OCAMLOPT) -I $(FSTAR_HOME)/ulib/ml -I out out/Bug.ml -o out/Bug
out/Bug
It seems the number -1l is converted to 2^32-1 = 4294967295, and not to -1 as
expected.
We use the following version:
$ /localdisk/zimmerma/FStar/bin/fstar.exe --version
F* 0.9.7.0-alpha1
platform=Linux_x86_64
compiler=OCaml 4.05.0
date=<not set>
commit=745b7a747ac2724484452e06669e738dd86fc02a (dirty)
(This probably worked in an earlier version of Fstar.)
Félix and Paul
_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
