k-legacy
k-legacy copied to clipboard
kframework
The K tools (deprecated, see README)
iitp@iitp-OptiPlex-9020:~/k/tutorial/1_k/2_imp/lesson_5$ kompile imp.k --pdf [Error] Critical: Unknown option: --pdf How to solve the above error? iitp@iitp-OptiPlex-9020:~/k/tutorial/1_k/2_imp/lesson_5$ kompile --version K framework version 4.0-SNAPSHOT Git revision: Git branch: UNKNOWN_BRANCH Build date: Wed...
Hi! I am interested in checking the validity (by unsatisfiability of a negated expression) of an expression inside a rule of my language specification in K 4.0. I used to...
Swap
Hi, I'd like to implement some kind of swap function. But I'm unable to specify multiple conditions in one cell. Is that possible. In case it is, how? Currently I...
I am using k-legacy the latest commit. I have the following definition and spec: ``` module TEST syntax Val ::= "@undef" syntax Val ::= NUVal syntax NUVal ::= "@val" "("Int","Int","Bool")"...
I am trying to use KEQ for establishing equivalence between two programs written in two languages: ``` module COMMON syntax Vals ::= @nil ... endmodule module L1 imports COMMON ......
I can not give a small example here, but sometimes when I use krun, a rule that I expect to apply, does not get normally applied, but when I use...
Hi! I am trying to apply the verification infrastructure of K 4.0; however, I cannot get it to work properly, and I ignore why. I want to verify a KernelC...
I used K3.6 to write the semantics of a language. Now I want to move to K4.0. But there is a problem for kompile. In K4.0, there is a new...
there are multiple rules with the same configuration state which means they can be activated at the same time ,so i try to set the priority of rules. but how...
The rewrite rule below will not fire unless the ```...``` between ```select ... selBranch``` is the same between both of the goRoutine cells. In other words, the ```...``` with the...
