prusti-dev icon indicating copy to clipboard operation
prusti-dev copied to clipboard
verified publisher icon viperproject

Ghost Type Encodings

Open aakp10 opened this issue 5 years ago • 2 comments

This PR adds encoding definitions for Ghost Types.

aakp10 avatar Sep 23 '20 07:09 aakp10

I totally agree that we should have some tests before merging.

fpoli avatar Sep 28 '20 08:09 fpoli

I totally agree that we should have some tests before merging.

@vakaras @fpoli Thanks for the reviews, I've added a couple of type checking related test cases for the ghost types. I'll continue extending the test cases to accommodate the noninterference properties of ghost types with the upcoming changes that I'm currently working on.

aakp10 avatar Sep 28 '20 19:09 aakp10