search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

Fix for #configuration builtin #2355

Closed theo25 closed 6 years ago

daejunpark commented 6 years ago

@theo25 let's see if it passes the tests: https://github.com/kframework/k/commits/theo-reflection-fix

daejunpark commented 6 years ago

@theo25 says:

So, TermContext has a private field called topTerm that was never set and kept its default null value. The #configuration builtin attempts to access this field to get the current configuration but since it’s null, a NullPointerException is thrown and never gets caught. So I added the correct (I think) initialization of the field when a ConstrainedTerm is built out of a Term and a TermContext.

Also, I have changed the implementation of the builtin. I am not sure what a KLabelInjection is but it did not return a term with a KLabel corresponding to the top cell of the configuration (e.g. “\<T>”). Instead it was returning term with a KLabel that somehow was made out of the whole configuration (e.g. “#\<T>(\<k> ...)”). I replaced that with simply returning the Term stored in the topTerm field of the context.

daejunpark commented 6 years ago

The jenkins failure seems to be due to ng setup failure. @ehildenb could you confirm that we can ignore this failure to merge this?

ehildenb commented 6 years ago

I'm looking into it, will try to re-trigger the test with corrected settings.

theo25 commented 6 years ago

@daejunpark FYI, I tried this fix on top of keq with our equivalence checking examples and everything works fine.

daejunpark commented 6 years ago

The jenkins failure has nothing to do with this PR and I merge this.