K-user mailing list

[Dwight Guth <dwight.guth AT runtimeverification.com>]

That's an excellent catch with that program. I will look into it on Monday and hopefully have a fix out in less than a day.

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

Thanks! I managed to get that to work. I wonder about this program, tho:

 #include <stdio.h>

 unsigned long f() {

  double d = -0.5;

  return d * (1 << 30);

 }

 int main() {

  printf("0x%lx\n",f());

 }

When I run it in kcc, it produces 0x20000000, but I think it is undefined behavior (because it converts a negative double to an unsigned long).

Also, as a more minor note, the vagrant vm seems to be unhappy when it is resumed after suspending (ie on "vagrant resume" after a "vagrant suspend"). It does a bunch of work that appears to be duplicated and then when I login after that, it asks me again for my password and tries to do that same setup step. Cancelling it via control-c seems to get me back to a prompt where I can run kcc again, tho.

Robby

On Sat, Jan 9, 2016 at 3:52 PM, Rosu, Grigore <grosu AT illinois.edu> wrote:

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....