search

kframework / k-legacy

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

Fix a bug in negMInt #2374

Closed sdasgup3 closed 6 years ago

sdasgup3 commented 6 years ago

Hello K-Team, This seems a bug to me provided NegMInt is meant to negate the bits of input MInt.

Please accept my change if this seems relevant and correct to you.

kframework-bot commented 6 years ago

Can one of the admins verify this patch?

daejunpark commented 6 years ago

Thanks @sdasgup3! Looks good to me. Could you write a simple test for it?

sdasgup3 commented 6 years ago

@daejunpark Thanks a lot for the feedback! I have added the test-case, but I am not sure if the path is the right one to be invoked by mvn verify -DskipKTest. I tried running ant test as instructed in here, but got 

Buildfile: build.xml does not exist!
Build failed

Can you give me some pointers on how/where to add it?

daejunpark commented 6 years ago

@sdasgup3 Thanks for adding the tests. It looks good to me.

You can run the tests by mvn verify in the top directory or ktest tests/config.xml under k-distribution directory.

Or, you can run only your test by:

$ cd k-distribution/tests/builtins/mint
$ ktest --skip pdf config.xml

I added a quick re-organization on the top and re-opened PR #2378.