diff options
| author | Kathy Gray | 2016-01-06 17:28:58 +0000 |
|---|---|---|
| committer | Kathy Gray | 2016-01-06 17:28:58 +0000 |
| commit | f98d4a9271751622647c021c32103fc05b681041 (patch) | |
| tree | 155a0ed5f2927fb86bb1596562d436e462d840ec /src/pretty_print.ml | |
| parent | 9219f8adddac4f6b6fc10e9c4965215b09829468 (diff) | |
Add new assert expression to Sail
This splits the former functionality of exit into errors, which should now use assert(bool,option<string>), and a means of signalling actions such as instruction-level exceptions, interrupts, or other features that impact the ISA. The latter will now be tracked with an effect escape, and so any function containing exit and declared pure will generate a type error.
WARNING: ARM spec will not build with this commit until I modify it. MIPS spec will not build with this commit until modified.
Diffstat (limited to 'src/pretty_print.ml')
| -rw-r--r-- | src/pretty_print.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml index f0005d02..24c978fd 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -428,6 +428,8 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = | E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_let" pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot | E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp pp_lem_l l pp_annot annot | E_exit exp -> fprintf ppf "@[<0>(E_aux (E_exit %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot + | E_assert(c,msg) -> + fprintf ppf "@[<0>(E_aux (E_assert %a %a) (%a, %a))@]" pp_lem_exp c pp_lem_exp msg pp_lem_l l pp_annot annot | E_internal_exp ((l, Base((_,t),_,_,_,_,bindings))) -> (*TODO use bindings where appropriate*) (match t.t with @@ -972,6 +974,8 @@ let doc_exp, doc_let = surround 2 1 opening cases rbrace | E_exit e -> separate space [string "exit"; exp e;] + | E_assert(c,m) -> + separate space [string "assert"; parens (separate comma [exp c; exp m])] (* adding parens and loop for lower precedence *) | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _) | E_cons (_, _)|E_field (_, _)|E_assign (_, _) |