-
Notifications
You must be signed in to change notification settings - Fork 88
Iter optimization clean up #974
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
Conversation
|
Yes, there should be a similar rebase of #965 within the next days. |
michael-schwarz
left a comment
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.
Thanks for the PR! As discussed on the other PR, we will likely merge the alternative #975 though :)
| module WeakUpdates = BaseDomain.WeakUpdates | ||
| module BaseComponents = BaseDomain.BaseComponents | ||
|
|
||
| open Iter |
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.
As far as I can see, this open is unused?
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.
Yes, that is correct, this open isn't needed.
| in | ||
| let alen = List.filter_map (fun v -> lenOf v.vtype) (AD.to_var_may a) in | ||
| let d = List.fold_left ID.join (ID.bot_of (Cilfacade.ptrdiff_ikind ())) (List.map (ID.of_int (Cilfacade.ptrdiff_ikind ()) %BI.of_int) (slen @ alen)) in | ||
| let d = Iter.((Iter.map String.length (Iter.of_list @@ AD.to_string a)) <+> (Iter.filter_map (fun v -> lenOf v.vtype) (Iter.of_list @@ AD.to_var_may a)) (*<- equal to slen @ alen *) |
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.
If you already have Iter.(...) outside, you do not need it inside again.
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.
Right, that somehow slipped my mind. Should I push a fix for that even though the code deadline has passed?
|
As we will not move ahead with Iter, closing this. |
This PR is a cleaned up version of PR #964
As discussed, I created a new PR containing only the relevant Iter related changes. This PR is now based on the merged
flambdaPR #928.In particular, it is based on the commit https://github.com/goblint/analyzer/commit/ab2141a00b577cb20d354878a315a2e27e5074c6
.
All relevant information can be found in the comments of #964.