kframework / kat Goto Github PK

Provide an example using Euler's GCD algorithm.

From @grosu:

function gcd(a, b)
    while b ≠ 0
       t := b; 
       b := a mod b; 
       a := t; 
    return a;

LGGs (on antiunfiers) can be a useful widening technique.

One way to take advantage: when we make a new rule LHS => RHS if C, we could try to transform it as much as possible (using unification) to C [ LHS' => RHS' ]. Then if C has the structure like C(T1,...TI, LHS' => RHS', TI+1,...TN), then all of T1...TI, and TI+1...TN could be replaced with variables. This may make the abstraction process more automatable in the presence of things like threads.

For some reason bumping to the newest K5 master branch breaks the strategy-based symbolic execution.

This means that a separate persistent branch of K5 must be maintained just for this repository.

Currently we have no visible record of what the collected constraints are when printing out the configuration.

We should find some way to print the constraint with each generated configuration.
I think having a module CONSTRAINTS in the prelude, that if you include makes a cell <constraint> available to you would be good. This would make us able to store each particular states constraint with that state for the SBC analysis.

@dwightguth, is it possible?

Need to migrate install instructions from https://github.com/kframework/evm-semantics (including changes to install libz3-dev on Ubuntu).