k-legacy
k-legacy copied to clipboard
kframework
The K tools (deprecated, see README)
This adds a missing smtlib attribute necessary for EVM verification, and changes how Z3 presents implications in a way that helps some EVM proofs. For some reason, calling check-sat between...
The proved does not always detect potentially stuck states and, due to that, can prove erroneous statements. Below @virgil-serbanuta and myself took advantage of the underspecification of division (division by...
* Files don't need end with "spec.k". * "true" is not printed when no claims are found. A more appropriate message is used instead. * Claims can be introduce by...
If you only change attributes, recompiling the semantics will ignore the changes and use the old rule attributes.
I have a [configuration](https://github.com/kframework/p4-semantics/) like following: ``` @resetArrays ( SetItem ( extra ) ) ~> ... ... extra |-> $array ( 4 , 0 , -1 ) ``` And I...
I have a [configuration](https://github.com/kframework/p4-semantics) that contains the following cells: ``` ... .K .K .Map .Map .K ``` Note ` .Map ` And I have the following rule ``` rule @processDec(counter...
Hi I installed the latest version (4.0.1) and tried to run, the output is fine but not appropriately formatted. The output looks just like below. There is no color, indent,...
https://github.com/kframework/evm-semantics/issues/95 As demonstrated there, `krun --prove` generates an enormous amount of (highly redundant) output sometimes when Z3 translations are not present. Is there a way we can be smarter about...
The old version of the plugin had issues dealing with versions of Java outside the range 1.8 range. The update fixes the issue.