aeneas icon indicating copy to clipboard operation
aeneas copied to clipboard

Improve error message about printing macros (`println!`/`dbg!`)

Open Cemoixerestre opened this issue 11 months ago • 0 comments
trafficstars

When I compile the simple "Hello World" program:

fn main() {
    println!("Hello World!")
}

I obtain the following error message:

[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.

Cemoixerestre avatar Dec 16 '24 16:12 Cemoixerestre