New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Spec compilation error #59

Open

suhabe opened this issue Oct 16, 2019 · 0 comments

suhabe commented Oct 16, 2019

Hi, I wrote this spec using the solidity-semantics, but can't get it to compile:

requires "solidity.k"

module T1-SPEC
    imports SOLIDITY

    rule    <k> #execute => . </k>
            <program> int sum ; sum = 3 + 4 ; </program>

endmodule

I used the following command:
./ksol prove tests/proofs/t1-spec.k
which gave me this compilation error:

[Error] Compiler: Had 1 parsing errors.
[Error] Inner Parser: Parse error: unexpected token ';'.
	Source(/home/sbugrara/solidity-semantics/tests/proofs/t1-spec.k)
	Location(7,31,7,32)

I can't figure out what I'm missing. I followed the build instructions at https://github.com/kframework/solidity-semantics

The text was updated successfully, but these errors were encountered:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment