diff options
| author | Thomas Bauereiss | 2017-08-29 17:42:56 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-08-29 17:47:52 +0100 |
| commit | 2300d45d6645faae3c00a183e80547c1a6cb9165 (patch) | |
| tree | 8e038185e5fa14ee216cd04217665de8f7d91c85 /src/pretty_print_lem.ml | |
| parent | 5ec766ceb381f15e6ab4cf568b0f6ab919ca6b68 (diff) | |
Make Lem export of CHERI(-256) typecheck
Note: The effect annotations of the execute function differ between CHERI and
MIPS, so I split out a new file mips_ast_decl.sail for MIPS with just the
initial declarations of ast, decode, and execute (with the right effects for
MIPS).
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 7671c26b..3d4f3083 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -843,8 +843,10 @@ let doc_exp_lem, doc_let_lem = if aexp_needed then parens (align epp) else align epp | E_exit e -> liftR (separate space [string "exit"; expY e;]) | E_assert (e1,e2) -> - let epp = separate space [string "assert'"; expY e1; expY e2] in - if aexp_needed then parens (align epp) else align epp + (* FIXME needs pretty-printing of E_constraint; ignore for now *) + string "()" + (* let epp = separate space [string "assert'"; expY e1; expY e2] in + if aexp_needed then parens (align epp) else align epp *) | E_app_infix (e1,id,e2) -> (* TODO: Should have been removed by the new type checker; check with Alasdair *) raise (Reporting_basic.err_unreachable l |