runtimeverification / erc20-semantics

ERC20 in K
Other
47 stars 15 forks source link

kompile error! #4

Open charlotte-Zch opened 5 years ago

charlotte-Zch commented 5 years ago

zch@ubuntu:~/erc20-semantics-k5/tests/imp$ kompile imp.k ocamlc: unknown option '-match-context-rows'. usage: ocamlfind ocamlc [options] file ... -package Refer to package when compiling -linkpkg Link the packages in -predicates

Add predicate

when resolving package properties -dontlink Do not link in package and its ancestors -syntax

Use preprocessor with predicate

-ppopt Append option to preprocessor invocation -ppxopt , Append options to ppx invocation for package -dllpath-pkg Add -dllpath for this package -dllpath-all Add -dllpath for all linked packages -ignore-error Ignore the 'error' directive in META files -passopt Pass option directly to ocamlc/opt/mklib/mktop -passrest Pass all remaining options directly -only-show Only show the constructed command, but do not exec it STANDARD OPTIONS: -a Build a library -absname Show absolute filenames in error messages -annot Save information in .annot -bin-annot Save typedtree in .cmt -c Compile only (do not link) -cc Use as the C compiler and linker -cclib Pass option to the C linker -ccopt Pass option to the C compiler and linker -compat-32 Check that generated bytecode can run on 32-bit platforms -config Print configuration values and exit -custom Link in custom mode -custom Link in custom mode -dllib Use the dynamically-loaded library -dllpath

Add to the run-time search path for shared libraries -dtypes (deprecated) same as -annot -for-pack Generate code that can later be `packed' with ocamlc -pack -o .cmo -g Save debugging information -i Print inferred interface -I Add to the list of include directories -impl Compile as a .ml file -intf Compile as a .mli file -intf-suffix Suffix for interface files (default: .mli) -intf_suffix (deprecated) same as -intf-suffix -keep-docs Keep documentation strings in .cmi files -keep-locs Keep locations in .cmi files -labels Use commuting label mode -linkall Link all modules, even unused ones -make-runtime Build a runtime system with given C objects and libraries -make_runtime (deprecated) same as -make-runtime -modern (deprecated) same as -labels -no-alias-deps Do not record dependencies for module aliases -no-app-funct Deactivate applicative functors -no-check-prims Do not check runtime for primitives -noassert Do not compile assertion checks -noautolink Do not automatically link C libraries specified in .cma files -nolabels Ignore non-optional labels in types -nostdlib Do not add default directory to the list of include directories -o Set output file name to -open Opens the module before typing -output-obj Output an object file instead of an executable -output-complete-obj Output an object file, including runtime, instead of an executable -pack Package the given .cmo files into one .cmo -pp Pipe sources through preprocessor -ppx Pipe abstract syntax trees through preprocessor -principal Check principality of type inference -rectypes Allow arbitrary recursive types -runtime-variant Use the variant of the run-time system -safe-string Make strings immutable -short-paths Shorten paths in types -strict-sequence Left-hand part of a sequence must have type unit -strict-formats Reject invalid formats accepted by legacy implementations (Warning: Invalid formats may behave differently from previous OCaml versions, and will become always-rejected in future OCaml versions. You should use this flag to detect and fix invalid formats.) -thread Generate code that supports the system threads library -unsafe Do not compile bounds checking on array and string access -unsafe-string Make strings mutable (default) -use-runtime Generate bytecode for the given runtime system -use_runtime (deprecated) same as -use-runtime -v Print compiler version and location of standard library and exit -verbose Print calls to external commands -version Print version and exit -vmthread Generate code that supports the threads library with VM-level scheduling -vnum Print version number and exit -w Enable or disable warnings according to : + enable warnings in - disable warnings in @ enable warnings in and treat them as errors

can be: a single warning number .. a range of consecutive warning numbers a predefined set default setting is "+a-4-6-7-9-27-29-32..39-41..42-44-45-48-50" -warn-error Enable or disable error status for warnings according to . See option -w for the syntax of . Default setting is "-a" -warn-help Show description of warning numbers -where Print location of standard library and exit - Treat as a file name (even if it starts with `-') -nopervasives (undocumented) -use-prims (undocumented) -dsource (undocumented) -dparsetree (undocumented) -dtypedtree (undocumented) -drawlambda (undocumented) -dlambda (undocumented) -dinstr (undocumented) -help Display this list of options --help Display this list of options [Error] Critical: ocamlopt returned nonzero exit code: 2 Examine output to see errors. [Warning] Compiler: Could not find main syntax module with name IMP-SYNTAX in definition. Use --syntax-module to specify one. Using IMP as default. [Warning] Compiler: missing entry for hook BAG.concat [Warning] Compiler: missing entry for hook BAG.element [Warning] Compiler: missing entry for hook BAG.unit
charlotte-Zch commented 5 years ago

After checking out to k5 branch and makefile KOMPILE_BACKEND?=java , it still have some syntax error