Use #kani_comment instead of #comment for deinit
#1708
Conversation
giltho
changed the title
#kani_comment instead of #comment for deinit
| /// inside the location sub of the irep. | ||
| pub fn with_comment<T: Into<InternedString>>(self, c: T) -> Self { | ||
| self.with_named_sub(IrepId::Comment, Irep::just_string_id(c)) | ||
| pub fn with_kani_comment<T: Into<InternedString>>(self, c: T) -> Self { |
There was a problem hiding this comment.
This ends up with "kani" stuff inside cprover_bindings. Is there a better way?
There was a problem hiding this comment.
Good point.
The only other way is to use a IrepId::FreeformString.
|
Was "comment" ever used? I wonder if we could just change that to |
|
I think checking with the CBMC team that there wouldn't be a conflict would be enough yes |
|
Check with the cbmc team that it's ok to just use |
|
There is nothing special about '#comment' in CBMC. It's the '#' prefix itself that is special, but beyond that there are no conflicts for this. |
|
Ah, sorry I hadn't seen Michael's answer. |
|
I renamed IrepId::HiddenComment => "#comment",
IremId::Comment => "comment"it's not much better but it does remove mentions of |
|
Maybe it's just fine as-is then? |
|
Yep, any change was breaking the CI anyway 🤔 |
|
So I'm closing this based on the comments. Please feel free to reopen if you think it is still relevant (and I'm sorry if I closed it prematurely). :) |
5 participants
Description of changes:
Instead of inserting a
commentfield on the Irep fordeinitand potential future annotations, inserts a#kani_comment.It seems that having a field that doesn't that with a
#might be dangerous otherwise.Resolved issues:
Resolves #1575
Call-outs:
Kani still outputs some
commentfields, as it used to before #1469, but thesecommentfields are inside a#c_locationfield, so they will be ignored by transitivity.Testing:
This is just a slight change, it should not change anything in kani.
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.