-
Notifications
You must be signed in to change notification settings - Fork 273
Upstreaming expr2cleanct #2704
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
Upstreaming expr2cleanct #2704
Conversation
This really needs tests, particularly for the unused method (is used in the TG repository where this came from), but hopefully unblocks @mmuesly for now. |
Branch exploring a nicer option: https://github.com/thk123/cbmc/tree/dump/expr2c-configuration To do to make it work (mostly internal to TG but potentially consider whether |
/// \return C code for representing a true or false value | ||
std::string expr2cleanct::convert_constant_bool(bool boolean_value) | ||
{ | ||
// This requires #include <stdbool.h> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In the generated class, or in this class?
If this comments aims on the generated class, why do you need this in the generated class, if using 0 and 1?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You're quite right - this comment was from when this uses true
and false
- I'll update
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You will have to touch the Makefile as well to make this usable.
Nit-pick: The clang formatting check failed, but for some reason, this doesn't seem to be required for merging. |
|
||
/// To convert a type in to ANSI-C but with the identifier in place. | ||
/// This is useful for array types where the identifier is inside the type | ||
/// \param src: the type to convert6 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
convert
/// It does not print padding components in structs | ||
/// It does not print array sizes when printing array types | ||
/// It does not print the body of the struct when printing the struct type | ||
class expr2cleanct:public expr2ct |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't see much value in having this as a separate class. I'd prefer to see the behaviour of expr2ct be made configurable if necessary.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Did you see this branch: https://github.com/thk123/cbmc/tree/dump/expr2c-configuration. It gets complicated as TG uses a broader interface than just expr2c/type2c
so the options are:
- rework TG to use the regular interface (probably at least a couple of days)
- add an extra method in
expr2c.h
for this extra route (half day?) - just add the extra method to
expr2ct
and use the class directly (quickest - but I think have the class defined in a separate header is supposed to indicate it isn't part of the public interface so feels like the worst option)
I'll have a look at the second one unless you think the third one is acceptable?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have had a brief look at the configuration branch and really liked it! Given my limited insight: can you briefly explain what this "broader interface" is that TG uses/requires? Looking at dump-c, this work will help simplify its code a lot, which of course I'll take on once any approach here is merged. I do suspect that TG may have similar pieces of code?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I missed that one. Yes, @thk123, that's what I had envisaged.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Wound up being relatively straight forward: #2713
Replaced by #2713 |
@peterschrammel As requested here is
expr2cleanct
. I was hoping to eliminate it and squash it intoexpr2ct
but this proved to be not as trivial as I'd hoped. I'll push where I got to if someone has the inclination to pick uit up.In any case, here is the
expr2cleanct
.