K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

Robby,

If your goal is only to run kcc as is, and not to modify the C semantics, then the simplest way to go is to download the RV-Match tool from https://runtimeverification.com/match/, which already incorporates a fast version of the kcc tool.

Thanks,

Grigore

 

 

---

From: Robby Findler [robby AT eecs.northwestern.edu]
Sent: Saturday, January 09, 2016 3:31 PM
To: Dwight Guth
Cc: k-user AT cs.uiuc.edu
Subject: Re: [[K-user] ] kcc

I wish to run whatever is simple and stable. Apparently I missed a choice point earlier in your documentation. Anyway, what do you recommend?

Thanks,

Robby

On Sat, Jan 9, 2016 at 3:27 PM, Dwight Guth <dwight.guth AT runtimeverification.com> wrote:

You need to be using the latest master of K if you want to build the latest master of the C semantics. :)

On Sat, Jan 9, 2016 at 3:26 PM, Robby Findler <robby AT eecs.northwestern.edu> wrote:

I'm trying to get kcc to build. I think I got as far as the last step
of running "make -j4" in the c-semantics directory, but I get the
error below.

Any hints?

tia,
Robby

☕  make -j4

Building the C parser...

366 states, 5603 transitions, table size 24608 bytes

3239 additional bytes used for bindings

2 shift/reduce conflicts.

2 shift/reduce conflicts.

Makefile:59: .depend-translation: No such file or directory

Makefile:60: .depend-execution: No such file or directory

Makefile:61: .depend-nd: No such file or directory

Makefile:62: .depend-nd-thread: No such file or directory

kdep -d "x86-gcc-limited-libc/c11-nd-thread-kompiled" -I
/Users/robby/git/kframework/c-semantics/x86-gcc-limited-libc/semantics
-- c11.k > .depend-nd-thread

kdep -d "x86-gcc-limited-libc/c11-nd-kompiled" -I
/Users/robby/git/kframework/c-semantics/x86-gcc-limited-libc/semantics
-- c11.k > .depend-nd

kdep -d "x86-gcc-limited-libc/c11-kompiled" -I
/Users/robby/git/kframework/c-semantics/x86-gcc-limited-libc/semantics
-- c11.k > .depend-execution

/bin/sh: kdep: command not found

make[1]: *** [.depend-nd-thread] Error 127

make[1]: *** Waiting for unfinished jobs....

/bin/sh: kdep: command not found

make[1]: *** [.depend-execution] Error 127

/bin/sh: kdep: command not found

make[1]: *** [.depend-nd] Error 127

make: *** [translation-semantics] Error 2

make: *** Waiting for unfinished jobs....