vale
vale copied to clipboard
Errors when running test files on Linux
I tested Vale with F* in Linux with the following command:
mono $HOME/vale-release-0.3.19/bin/vale.exe -fstarText -in common.vaf -out common.fst -outi common.fsti
fstar.exe --query_stats common.fst
I'm able to run it for common.vaf and forall.vaf but most of the instruction-specific files which include files like
include "../../../fstar/code/arch/x64/X64.Vale.InsBasic.vaf"
include{:fstar}{:open} "TestFStar"
include{:fstar}{:open} "FStar.Seq.Base"
are giving the following errors:
error at line 21 column 9 of file $HOME/hacl-star/vale/code/test/Vale.Test.X64.Memcpy.vaf:
cannot find id 'locs_disjoint'
error at line 18 column 14 of file $HOME/vale-0.3.19/tools/Vale/test/test.vaf:
cannot find type 'nat64'
error at line 41 column 5 of file $HOME/vale/tools/Vale/test/FTypeVale.vaf:
cannot find type 'byte'
I'm assuming these types have been defined in F* and somehow the compilation is not able to fetch these into the code.
Any help would be helpful.