gobra icon indicating copy to clipboard operation
gobra copied to clipboard
verified publisher icon viperproject

Support for Ghost Pointers

Open ArquintL opened this issue 1 year ago • 1 comments

This PR adds support for ghost pointers. However, ghost fields will be added by a separate PR. Note that this PR does not address the issue of calling ghost functions in non-ghost code, which is instead part of PR #755.

ArquintL avatar Mar 20 '24 17:03 ArquintL

I had to change the implementation quite a bit more and introduce the concept of whether the location an expression refers to is ghost or not. Please take another look

ArquintL avatar Mar 24 '24 21:03 ArquintL