Skip to content
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.

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

Panic when accessing inherited extern specs for polymorphic methods #1293

Open
Lysxia opened this issue Dec 6, 2024 · 0 comments
Open

Panic when accessing inherited extern specs for polymorphic methods #1293

Lysxia opened this issue Dec 6, 2024 · 0 comments
Labels
bug Something isn't working crash Creusot crashes with a panic and dumps a stack trace

Comments

@Lysxia
Copy link
Collaborator

Lysxia commented Dec 6, 2024

extern crate creusot_contracts;
use creusot_contracts::*;

use std::iter::FromIterator;

#[ensures(result@ == x@)]
pub fn id<A>(x: Vec<A>) -> Vec<A> {
    Vec::from_iter(x.into_iter())
}
thread 'rustc' panicked at /rustc/c1a6199e9d92bb785c17a6d7ffd8b8b552f79c10/compiler/rustc_type_ir/src/binder.rs:716:9:
type parameter `T/#2` (T/#2/2) out of range when instantiating, args=[std::vec::Vec<T/#0, std::alloc::Global>, T/#0]

The panic happens in creusot/src/translation/specification.rs, in the function contract_of. The problem is that the argument list returned by inherited_extern_spec only include arguments for the trait itself, and not additional arguments of the method.

@Lysxia Lysxia added bug Something isn't working crash Creusot crashes with a panic and dumps a stack trace labels Dec 6, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working crash Creusot crashes with a panic and dumps a stack trace
Projects
None yet
Development

No branches or pull requests

1 participant