Merged
Conversation
Contributor
Author
|
The first 7 commits are from #1558 (waiting to be merged). Do not merge this until that PR has been merged and this one has been rebased on it. |
Contributor
|
Tagging do-not-merge until predecessor PRs are merged |
smowton
approved these changes
Nov 6, 2017
Contributor
|
Note: needs @kroening review before merge |
cb9badb to
2e5c5c4
Compare
2e5c5c4 to
4a81511
Compare
4a81511 to
c1a02cc
Compare
Contributor
|
Now mergeable once test failures are addressed |
76f0980 to
73c5007
Compare
Creates the initialize methods again taking account of symbols added to the symbol table during instantiation of lazy methods since they were first created.
Made load_all_functions compatible with some functions having already been loaded by using the lazy load procedure
After convert each function in convert_lazy_method call instrument and typecheck
The symbolt was erased and recreated rather than being modified. This was bad as it invalidated the reference to the symbol that we now use later.
Load the main function into the symbol table before generating the entry point so that we have access to its parameter names Allow attempts to load a function already loaded for non-lazy cases
Otherwise symbols won't have reproducible names
Remove line that depends on generated symbol name - Lucas confirms it wasn't the purpose of the test anyway.
Don't store followed type as type of superclass when doing clean cast as it may later change since we can now convert more methods after typechecking and doing this may change the type
03a7733 to
a2cf16d
Compare
Contributor
Author
|
I think everything is answered, fixed or an issue created to track it now. Tests are all passing. |
peterschrammel
approved these changes
Dec 21, 2017
Member
|
TG passes too. Seems ready to go then. |
Member
|
I am sticking a 'do not merge' label on it to reduce risk for a planned TG release on 3rd Jan. We'll merge it right after that. Besides, an approval is required by @tautschnig or @kroening. |
tautschnig
approved these changes
Dec 21, 2017
Collaborator
|
Added a new label (Merge on 4 Jan) as there might be more coming up the next days that shouldn't get merged until then. Obviously I know nothing about about the release so feel free to change that. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR is quite long, I'd recommend reviewing commit-by-commit. It has been reviewed in part in Security Scanner but @smowton feels it is ready to be reviewed for inclusion in to CBMC now.
In the end this version eagerly loads all functions (although it does it by pulling them in explicitly). Individual users are free to alter this behaviour.