Re: [fstar-club] bug report (wrong cast from I32)

[Jonathan Protzenko via fstar-club]

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&amp;data=02%7C01%7Cprotz%40microsoft.com%7C6829aaf53873438dcb8b08d6ff085a14%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636976808689297728&amp;sdata=ff4spRPic%2Fc1zAMD6xbDRhIbZelrGvhwjyLZCLJzj04%3D&amp;reserved=0

_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club