Skip to content
This repository has been archived by the owner on May 4, 2024. It is now read-only.

[Prover] internal boogie error for type_info #701

Closed
junkil-park opened this issue Nov 28, 2022 · 1 comment
Closed

[Prover] internal boogie error for type_info #701

junkil-park opened this issue Nov 28, 2022 · 1 comment

Comments

@junkil-park
Copy link
Collaborator

How to reproduce

Uncomment this line https://github.com/aptos-labs/aptos-core/pull/5712/files#diff-2f8d5cc984e8ad9aeddd19f91aeb2bb0a8421a8429399426631774b0218423b2R139.

Run Prover, and it will produces the following error:

$  move prove
[INFO] preparing module 0x1::debug
[INFO] preparing module 0x1::math128
[INFO] preparing module 0x1::math64
[INFO] preparing module 0x1::type_info
[INFO] preparing module 0x1::from_bcs
[INFO] preparing module 0x1::any
[INFO] preparing module 0x1::aptos_hash
[INFO] preparing module 0x1::bls12381
[INFO] preparing module 0x1::capability
[INFO] preparing module 0x1::comparator
[INFO] preparing module 0x1::copyable_any
[INFO] preparing module 0x1::ed25519
[INFO] preparing module 0x1::multi_ed25519
[INFO] preparing module 0x1::simple_map
[INFO] preparing module 0x1::pool_u64
[INFO] preparing module 0x1::ristretto255
[INFO] preparing module 0x1::secp256k1
[INFO] preparing module 0x1::table
[INFO] preparing module 0x1::table_with_length
[INFO] transforming bytecode
[INFO] generating verification conditions
[INFO] 167 verification conditions
[INFO] running solver
Error: [internal] boogie exited with compilation errors:
output.bpl(6041,68): Error: cannot refer to a global variable in this context: #0_info
1 name resolution errors detected in **output.bpl**

Expected output

Prover produces no error.

@junkil-park
Copy link
Collaborator Author

Use the native spec functionspec_is_struct<T>() instead, and the issue is gone.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Projects
None yet
Development

No branches or pull requests

1 participant