K-user mailing list

[<daparpon AT dsic.upv.es>]

Hi, Xiaohong. I have been trying to update my project to K 4.0 for a long
time, but there is a core feature in my language that keeps me stuck in K 3.4.
More specifically, at some point of the symbolic execution of a program I need
to read the path condition and process it. I asked back in February to this
list whether that was possible in K 4.0, but the team told me that this
feature was not available yet. Moreover, I would like to have control over the
symbolic values and its inner identifiers, since I need them to represent (for
instance) symbolic addresses for program variables and I cannot manage just
some fresh names like V0 or V1, instead of #symInt(x) or #symInt(listSize). If
these capabilities are now implemented, I can try jumping into K 4.0 again,
but I would stick to K 3.4 until the equivalence between the old symbolic
Maude backend and the new symbolic Java backend is refined.

Thanks a lot for your interest. Best regards,
Daniel

________________________________________
From: Chen, Xiaohong
Sent: Thursday, June 15, 2017 3:42 PM
To: 
daparpon AT dsic.upv.es
Subject: RE: [[K-user] ] Documentation for K source code

Dear Daniel,

I raised your problem in our lab meeting.

K 3.4 is a very old project (+5 years ago), and we have very few people
maintaining it. The best we can do is try using the latest version of K and
let me know if you have any specific problems with that.

Yours,
Xiaohong
-------------------------
Chen, Xiaohong
BSc, Peking University
PhD student, UIUC

________________________________________
From: Chen, Xiaohong
Sent: Thursday, June 15, 2017 9:19 AM
To: 
daparpon AT dsic.upv.es
Subject: RE: [[K-user] ] Documentation for K source code

Hi Daniel,

If there is no specific reason to use K 3.4, we always recommend you using the
latest version of K, which can be downloaded here
https://github.com/kframework/k .

K 3.4 provides some APIs for you to call, such as krun, kompile, etc... They
can be found in KTool/src/javasources/KTool/src/org/kframework/ The code there
is in fact wrapped with some comments, telling you the meaning of parameters
etc.

PS, I am looking into your previous problem of calling Z3 in K and got a
different result. I will turn to you when I have an answer.

Cheers,
Xiaohong

-------------------------
Chen, Xiaohong
BSc, Peking University
PhD student, UIUC

________________________________________
From: 
daparpon AT dsic.upv.es
 
[daparpon AT dsic.upv.es]
Sent: Thursday, June 15, 2017 5:34 AM
To: 
k-user AT lists.cs.illinois.edu
Subject: [[K-user] ] Documentation for K source code

Hi! I'd wish to use the K Tool from my Java application (more specifically, in
order to call Krun and process the returning output), so I got the Source Code
version of K 3.4 from Github and built it to obtain the corresponding .jar
library. However, I noticed there is no documentation available for it in the
distribution folder, not even in the source .java files, thus I do not know
how I can call and use their operations. Is there any kind of manual or
documentation that I can consult?

Thanks in advance,
Daniel