daparpon
commented
6 years ago I said nothing, I have already found them. I was looking for the files in "k-distribution/target/release/k/samples", but it seems those files are deprecated or whatsoever. The actual, working files for testing the verification infrastructure are in "k-distribution/samples-kore".
Hi! I am interested in trying out the verification features of K 4.0 (latest distribution in GitHub), so I downloaded and installed it and checked that the binaries work as expected. However, when I went to compile the KernelC language specification provided for verification (in the samples/kernelc folder), I found that there are dependencies that apparently are not included in the distribution. More specifically, the following lines in samples/ kernelc/kernelc.k point to a file and a module that are nowhere to be found:
require "patterns/int_set.k" imports VERIFICATION_LEMMAS
I tried to comment them and compile the language anyway (in case they were deprecated dependencies), but kompile gives me the following error, indicating that they are still needed:
[Error] Compiler: Had 46 parsing errors. [Error] Critical: Could not infer a unique sort for variable 'IntSet'. Possible sorts: Bag@KCELLS, List@LIST, Set@SET, Map@MAP Source(/Users/elp/Documents/k/samples/kernelc/./patterns/int_list.k) Location(33,8,33,45) [Error] Critical: Could not infer a unique sort for variable 'IntSet'. Possible sorts: Id@ID, Set@SET, VariableDeclarations@KERNELC-SYNTAX, Globals@KERNELC-SYNTAX, Map@MAP, Statements@KERNELC-SYNTAX, Bag@KCELLS, List@LIST Source(/Users/elp/Documents/k/samples/kernelc/./patterns/ tree_pattern.k) Location(15,8,15,34) [Error] Inner Parser: Parse error: unexpected character ')'. Source(/Users/elp/Documents/k/samples/kernelc/./kernelc-semantics.k) Location(287,52,287,53) ... (more similar errors referring to IntSet occurrences)
How can I solve this problem? I have been trying to get the verification infrastructure of K to work for a long, long time, and I keep continuously running into issues about it...