Implement lookahead widening - #1484
RonaldJudin wants to merge 17 commits into
Conversation
|
Is there interest in merging this down the road? |
|
I'm still interested in having this but haven't worked on this since #1483 is still open as well. |
sim642
added
the
pr-dependency
Pilot value needs to use pilot value from returned function too, not main?
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| let special man r f args = lift_fun man S.special ((|>) args % (|>) f % (|>) r) | ||
|
|
||
| let enter man r f args = | ||
| M.tracel "LA" "enter: %a" D.pretty man.local; |
| let enter man r f args = | ||
| M.tracel "LA" "enter: %a" D.pretty man.local; | ||
| let (l1, l2) = lift_fun' man S.enter ((|>) args % (|>) f % (|>) r) in | ||
| M.tracel "LA" "enter l1: %a" (Pretty.d_list "\n" D.pretty) l1; |
| M.tracel "LA" "enter: %a" D.pretty man.local; | ||
| let (l1, l2) = lift_fun' man S.enter ((|>) args % (|>) f % (|>) r) in | ||
| M.tracel "LA" "enter l1: %a" (Pretty.d_list "\n" D.pretty) l1; | ||
| M.tracel "LA" "enter l2: %a" (Pretty.d_list "\n" D.pretty) l2; |
|
By merging in #2081, I got rid of the It still comes up with a lot of exceptions and fixpoint errors that need to be fixed. |
|
Ugh, that's strange. By merging #2081 to master the base branch for this got deleted and this got automatically closed. And I can't reopen it either or change the base branch for this back to master. Usually this hasn't been a problem because GitHub has automatically change the base branch and kept the PR open. Maybe that doesn't work for PRs from forks? Odd though because I could change the base branch to begin with. |
|
Apparently there's a workaround: isaacs/github#1557. So I managed to reopen it by temporarily recreating the old base branch. |
This branch has not been deployed
4 participants
Lookahead widening from https://link.springer.com/chapter/10.1007/11817963_41
TODO
threadenter.master.AnalysisState.widening. Now on top of Switch towidenwhich doesn't requireleqon arguments #2081.widenwhich doesn't requireleqon arguments #2081.Speclifter argument conversions until exception handlers insidelift_fun#2108?Invalid_argumentexceptions (on SV-COMP no-overflow).List.map2inenter(somehow only on multi-threaded).ERROR (verify)-s (on SV-COMP no-overflow).