Skip to content

Bug: Monomorphization Names in Eurydice #722

@ssyram

Description

@ssyram

The following codes produce Not_found error in the main function when calls Charon with --monomorphize. This seems to be something to do with the NameMatcher mechanism.

trait SomeTrait {
    fn some_method(&self);
}

struct Point<T> { x : i32, y : u64, z : T }

impl SomeTrait for Point<i32> {
    fn some_method(&self) {
        assert!(self.x > 0 && self.y < 100 && self.z != 0);
    }
}

fn main() {
    let p = Point { x: 10, y: 50, z: 1 };
    p.some_method();
}

Metadata

Metadata

Assignees

No one assigned

    Labels

    C-bugA bug in charon

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions