aeneas icon indicating copy to clipboard operation
aeneas copied to clipboard

Crash when extracting reference to `Self`

Open sonmarcho opened this issue 1 year ago • 0 comments

The following code makes Aeneas crash:

pub trait MinimumTraitExample {
    const CONSTANT: u32 = 10;

    fn uses_self() -> u32 {
        Self::CONSTANT
    }
}

Error:

Uncaught exception:
  
  (Failure "Unexpected occurrence of `Self`")

Raised at Aeneas__ExtractTypes.extract_trait_instance_id in file "ExtractTypes.ml", line 664, characters 8-57
Called from Aeneas__ExtractTypes.extract_trait_ref in file "ExtractTypes.ml", line 581, characters 2-68
Called from Aeneas__Extract.extract_App in file "Extract.ml", line 340, characters 10-71
Called from Aeneas__Extract.extract_adt_cons.(fun) in file "Extract.ml", line 532, characters 8-44
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Aeneas__Extract.extract_adt_g_value in file "Extract.ml", line 177, characters 10-170
Called from Aeneas__Extract.extract_adt_cons in file "Extract.ml", line 530, characters 4-174
Called from Aeneas__Extract.extract_fun_decl_gen in file "Extract.ml", line 1546, characters 12-77
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Aeneas__Translate.export_functions_group_scc in file "Translate.ml", line 561, characters 4-42
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Aeneas__Translate.export_functions_group in file "Translate.ml", line 642, characters 7-80
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 768, characters 2-52
Called from Aeneas__Translate.extract_file in file "Translate.ml", line 886, characters 2-36
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1431, characters 5-42
Called from Dune__exe__Main in file "Main.ml", line 277, characters 6-58

sonmarcho avatar Mar 27 '24 13:03 sonmarcho