Skip to content

Fix positions for inlined functions #1477

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 1 commit into from
Nov 9, 2023
Merged

Fix positions for inlined functions #1477

merged 1 commit into from
Nov 9, 2023

Conversation

mario-bucev
Copy link
Collaborator

In some cases, VCs positions could be incorrect when using inline functions.
This is particularly the case for synthetic copy methods which are always inlined.
For instance, in the following snippet, the VC generated for mc.copy(x = y) would incorrectly point at the definition of MyClass. This PR fixes this issue and the correct position is now reported.

case class MyClass(x: BigInt, y: BigInt)

def buildClass(mc: MyClass, x: BigInt): MyClass = {
  mc.copy(x = y)
}.ensuring(_.x >= 0)

@vkuncak
Copy link
Collaborator

vkuncak commented Nov 8, 2023

Are you saying that the position for a function f that is called from g and inlined will also be reported in g? Does this apply to user-defined functions as well?

@mario-bucev
Copy link
Collaborator Author

If I'm understanding correctly, yes, the inlined body of f will have its position set to the call site.
Note that inlined bodies are annotated as @DropVCs (except for synthetic inlined functions since these are removed and as such cannot be checked independently).

@mario-bucev mario-bucev merged commit a1f744d into epfl-lara:main Nov 9, 2023
@mario-bucev mario-bucev deleted the fix-inlined-pos branch November 9, 2023 15:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@vkuncak vkuncak vkuncak approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@mario-bucev @vkuncak