You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
[Info ] Imported: counter_example_aeneas.llbc
Uncaught exception:
(Failure Unreachable)
Raised at Charon__TypesUtils.ty_as_literal in file "charon/charon-ml/src/TypesUtils.ml", line 93, characters 9-38
Called from Aeneas__InterpreterExpressions.eval_operand_no_reorganize in file "interp/InterpreterExpressions.ml", line 279, characters 40-61
Called from Aeneas__Cps.map_apply_continuation.eval_list in file "interp/Cps.ml", line 87, characters 26-33
Called from Aeneas__InterpreterExpressions.eval_operands in file "interp/InterpreterExpressions.ml", line 396, characters 4-77
Called from Aeneas__InterpreterExpressions.eval_rvalue_aggregate in file "interp/InterpreterExpressions.ml", line 773, characters 24-57
Called from Aeneas__InterpreterExpressions.eval_rvalue_not_global in file "interp/InterpreterExpressions.ml", line 858, characters 21-79
Called from Aeneas__InterpreterStatements.eval_statement_raw in file "interp/InterpreterStatements.ml", line 880, characters 29-77
Called from Aeneas__InterpreterStatements.eval_statement in file "interp/InterpreterStatements.ml", line 859, characters 10-44
Called from Aeneas__InterpreterStatements.eval_statement_raw in file "interp/InterpreterStatements.ml", line 950, characters 29-58
Called from Aeneas__InterpreterStatements.eval_statement in file "interp/InterpreterStatements.ml", line 859, characters 10-44
Called from Aeneas__InterpreterStatements.eval_function_body in file "interp/InterpreterStatements.ml", line 1551, characters 26-56
Called from Aeneas__Interpreter.evaluate_function_symbolic in file "interp/Interpreter.ml", line 619, characters 8-65
Called from Aeneas__BorrowCheck.borrow_check_crate.borrow_check_fun in file "BorrowCheck.ml", line 24, characters 16-68
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Dune__exe__Main in file "Main.ml", line 508, characters 31-70
The dbg! macro also produces a similar message.
The text was updated successfully, but these errors were encountered:
When I compile the simple "Hello World" program:
I obtain the following error message:
The
dbg!
macro also produces a similar message.The text was updated successfully, but these errors were encountered: