-
Notifications
You must be signed in to change notification settings - Fork 6k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Pretty print expected json output of command line tests. #7665
Comments
The |
This should be very easy to do without extra dependencies now that #11583 is implemented. Just add the |
@matheusaaguiar May I take it? |
@GeorgePlotnikov yes, please! Let me know if you need any help. |
@matheusaaguiar let me clarify I'm moving in the right direction. There is a script The
but we want to give a user opportunity to write an output in a
My questions are:
|
Yes, you are going in the right direction. I don't think we want to give the user the option of |
Also, we then want to remove Another thing, I'd recommend Finally, we actually have some command-line tests that test the |
hi @matheusaaguiar @cameel before proceeding with the main subject of this issue I decided to build and run all tests including both z3 and CVC4. I founded a small suspicious place but I'm not sure whether it is a known bit. If it is I can create a PR to fix it. If not please advise. Here we have the following: solidity/libsmtutil/CVC4Interface.cpp Line 242 in b12b845
but it the CVC4 bitvector.h there are two constructors that make this call ambiguous:
I suggest to put an explicit cast for a proper call. I have already test it on my environment, works fine. |
I'm not sure it really matters in this case since this seems to be used to simply represent zero. Either type should work. Does it generate a warning? @leonardoalt Want to take a look? |
@cameel it even generates an error due to an ambiguous call |
Oh. Right, we definitely want to fix that. Feel free to create a PR. I wonder why our CI does not detect this. We surely have some runs with CVC4 enabled... What platform are you on? |
@cameel I'm on MacOS 12.5 |
Thanks. I guess that's it. We don't install CVC4 on macOS. Maybe we should. What do you think @leonardoalt? |
PR #13556 created |
@cameel @matheusaaguiar sorry for being a nerd but why there are byte/op codes, a source map sometimes are present in tests like here:
but sometimes are not like here:
what should I do? substitute byte code (etc.) with the |
It looks like the regexes in |
@cameel @matheusaaguiar PR #13586 was created please take a look |
@cameel now it can be closed I guess |
cool, thanks @matheusaaguiar for helping |
Came up in #7589 (comment).
Is there a nice and easy way to have a pretty printing pass on the output? That would make those tests way easier to review.
The text was updated successfully, but these errors were encountered: