K-user mailing list

[Alex <alexdba AT gmail.com>]

Thanks for the explanation!

I had figured out that I could match parts of the final configuration, and that is also useful.

Unfortunately that is not what I'm looking for: by guiding the execution path, I mean that

I'm looking for a way to specify a path condition, as in symbolic execution.

I guess that --pattern parameter is not the way to go.

I've saw mentions of using k-framework to perform symbolic execution, but I didn't find

a way to drive the execution path.

I would appreciate any suggestion.

Thanks again,

Alex

Le mar. 14 févr. 2017 à 11:15, Saxena, Manasvi <msaxena2 AT illinois.edu> a écrit :

Hi Alex,

The pattern specified by the —pattern option is matched on the final configuration, and the substitution is displayed, instead of the entire configuration.

For e.g., suppose the result of a krun execution is

<T> <result> 10 </result> *other stuff* </T>

then, you can filter your output by running giving krun the —pattern flag. You could call run with —pattern ‘<result> X </result>, and the result would be -
Solution 1
X ==K 10

> Is it possible to guide the execution path using such parametere, or is there another way?

I don’t think you’ll be able to use the —pattern flag to guide the execution. By guiding, do you mean you only want certain, but not all rules from the definition, to be considered during application? Or are you looking for a way to specify rewrite rules in the command line during krun?

-Manasvi


> On Feb 14, 2017, at 5:43 AM, Alex <alexdba AT gmail.com> wrote:
>
> Cheers!
>
> Do someone have a nice example of how to use the --pattern parameter in the krun tool?
>
> Is it possible to guide the execution path using such parametere, or is there another way?
>
> Thanks!
> Alex Alberto