Support asserts with messages

[zhassan-aws]

trafficstars

It's very common for code to contain asserts with custom messages, e.g.:

assert!(x == 0, "must be zero");

This currently leads to a crash in Aeneas, e.g.:

$ aeneas -backend lean assert_msg.llbc 
[Info ] Imported: assert_msg.llbc
Uncaught exception:
  
  (Failure Unreachable)

Raised at Charon__TypesUtils.ty_as_literal in file "charon/src/TypesUtils.ml", line 93, characters 9-38
Called from Aeneas__InterpreterExpressions.eval_operand_no_reorganize in file "InterpreterExpressions.ml", line 283, characters 40-61
Called from Aeneas__Cps.map_apply_continuation.eval_list in file "Cps.ml", line 88, characters 26-33
Called from Aeneas__InterpreterExpressions.eval_operands in file "InterpreterExpressions.ml", line 400, characters 4-77
Called from Aeneas__InterpreterExpressions.eval_rvalue_aggregate in file "InterpreterExpressions.ml", line 778, characters 24-57
Called from Aeneas__InterpreterExpressions.eval_rvalue_not_global in file "InterpreterExpressions.ml", line 863, characters 21-79
Called from Aeneas__InterpreterStatements.eval_statement_raw in file "InterpreterStatements.ml", line 898, characters 29-77
Called from Aeneas__InterpreterStatements.eval_statement in file "InterpreterStatements.ml", line 877, characters 10-44
Called from Aeneas__InterpreterStatements.eval_statement_raw in file "InterpreterStatements.ml", line 968, characters 29-58
Called from Aeneas__InterpreterStatements.eval_statement in file "InterpreterStatements.ml", line 877, characters 10-44
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__InterpreterStatements.eval_statement_raw in file "InterpreterStatements.ml", line 973, characters 8-545
Called from Aeneas__InterpreterStatements.eval_statement in file "InterpreterStatements.ml", line 877, characters 10-44
Called from Aeneas__InterpreterStatements.eval_switch in file "InterpreterStatements.ml", line 1100, characters 29-64
Called from Aeneas__InterpreterStatements.eval_statement in file "InterpreterStatements.ml", line 877, characters 10-44
Called from Aeneas__InterpreterStatements.eval_statement_raw in file "InterpreterStatements.ml", line 968, characters 29-58
Called from Aeneas__InterpreterStatements.eval_statement in file "InterpreterStatements.ml", line 877, characters 10-44
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__InterpreterStatements.eval_statement_raw in file "InterpreterStatements.ml", line 973, characters 8-545
Called from Aeneas__InterpreterStatements.eval_statement in file "InterpreterStatements.ml", line 877, characters 10-44
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__InterpreterStatements.eval_statement_raw in file "InterpreterStatements.ml", line 973, characters 8-545
Called from Aeneas__InterpreterStatements.eval_statement in file "InterpreterStatements.ml", line 877, characters 10-44
Called from Aeneas__InterpreterStatements.eval_function_body in file "InterpreterStatements.ml", line 1572, characters 26-56
Called from Aeneas__Interpreter.evaluate_function_symbolic in file "Interpreter.ml", line 660, characters 8-65
Called from Aeneas__Translate.translate_function_to_symbolics in file "Translate.ml", line 37, characters 25-77
Called from Aeneas__Translate.translate_function_to_pure_aux in file "Translate.ml", line 57, characters 23-69
Called from Aeneas__Translate.translate_function_to_pure in file "Translate.ml", line 210, characters 6-79
Called from Stdlib__List.filter_map.aux in file "list.ml", line 258, characters 14-17
Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 286, characters 4-134
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1033, characters 4-33
Called from Dune__exe__Main in file "Main.ml", line 317, characters 14-66

It would be nice if these are supported.