search

AeneasVerif / aeneas

A verification toolchain for Rust programs
Apache License 2.0
186 stars 15 forks source link

Missing function during analysis pop up #269

Closed RaitoBezarius closed 3 months ago

RaitoBezarius commented 3 months ago 
❯ aeneas -backend lean avl_verification.llbc
[Info ] Imported: avl_verification.llbc
Uncaught exception:

  Not_found

Raised at Stdlib__Map.Make.find in file "map.ml", line 137, characters 10-25
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__FunsAnalysis.analyze_module.analyze_fun_decl_group in file "FunsAnalysis.ml", line 206, characters 15-71
Called from Aeneas__FunsAnalysis.analyze_module.analyze_decl_groups in file "FunsAnalysis.ml", line 219, characters 8-35
Called from Aeneas__FunsAnalysis.analyze_module in file "FunsAnalysis.ml", line 235, characters 2-36
Called from Aeneas__Interpreter.compute_contexts in file "Interpreter.ml", line 34, characters 4-74
Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 229, characters 18-40
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1006, characters 4-33
Called from Dune__exe__Main in file "Main.ml", line 317, characters 14-66

on https://github.com/RaitoBezarius/avl-verification/tree/avl

RaitoBezarius commented 3 months ago

revision: 3f07bf067fe725c2bc60b12139ff9cba13375c6a