Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
Cemoixerestre opened this issue Dec 16, 2024 · 0 comments
Open

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

Cemoixerestre opened this issue Dec 16, 2024 · 0 comments

Comments

@Cemoixerestre
Copy link

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant