[Cherry-Pick][Prover] Declare the memory variables for type parameters in the generated boogie file

move-language / move

Apache License 2.0

2.25k stars 684 forks source link

[Cherry-Pick][Prover] Declare the memory variables for type parameters in the generated boogie file #958

Closed junkil-park closed 1 year ago

junkil-park commented 1 year ago

A type parameter that has the key-ability can have a memory space. This PR makes Prover declare the memory variables for type parameters in the generated boogie file.

Motivation

To declare the memory variables for type parameters

Have you read the Contributing Guidelines on pull requests?

yes

Test Plan

cargo test