Hello Paul and Félix, Thanks for the bug report -- I've filed https://github.com/FStarLang/FStar/issues/1803
Out of curiosity, what was your initial interest in F*? Are you interested in proving some numerical routines? Cheers, ~ jonathan ________________________________ From: fstar-club <fstar-club-boun...@lists.gforge.inria.fr> on behalf of paul zimmermann via fstar-club <fstar-club@lists.gforge.inria.fr> Sent: Tuesday, July 2, 2019 7:33 AM To: fstar-club@lists.gforge.inria.fr Cc: felix.bre...@inria.fr Subject: [fstar-club] bug report (wrong cast from I32) 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://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.gforge.inria.fr%2Fmailman%2Flistinfo%2Ffstar-club&data=02%7C01%7Cprotz%40microsoft.com%7C6829aaf53873438dcb8b08d6ff085a14%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636976808689297728&sdata=ff4spRPic%2Fc1zAMD6xbDRhIbZelrGvhwjyLZCLJzj04%3D&reserved=0
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club