diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-10-06 15:46:47 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-10-06 15:46:47 +0000 |
commit | f7693b3d897b90fd3bc2533be002dc0bdcd9f6c2 (patch) | |
tree | 93ea9491693324d2d690c4236a2c88c3b461e225 /cfrontend/PrintClight.ml | |
parent | 261ef24f7fd2ef443f73c468b9b1fa496371f3bf (diff) | |
download | compcert-f7693b3d897b90fd3bc2533be002dc0bdcd9f6c2.tar.gz compcert-f7693b3d897b90fd3bc2533be002dc0bdcd9f6c2.zip |
Merge of branch seq-and-or. See Changelog for details.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/PrintClight.ml')
-rw-r--r-- | cfrontend/PrintClight.ml | 53 |
1 files changed, 28 insertions, 25 deletions
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index ced5717e..ae8e31d4 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -20,6 +20,7 @@ open Camlcoq open Datatypes open Values open AST +open PrintAST open Csyntax open PrintCsyntax open Clight @@ -65,7 +66,6 @@ let rec precedence = function | Ebinop(Oand, _, _, _) -> (8, LtoR) | Ebinop(Oxor, _, _, _) -> (7, LtoR) | Ebinop(Oor, _, _, _) -> (6, LtoR) - | Econdition _ -> (3, RtoL) (* Expressions *) @@ -100,8 +100,6 @@ let rec expr p (prec, e) = expr (prec1, a1) (name_binop op) expr (prec2, a2) | Ecast(a1, ty) -> fprintf p "(%s) %a" (name_type ty) expr (prec', a1) - | Econdition(a1, a2, a3, _) -> - fprintf p "%a@ ? %a@ : %a" expr (4, a1) expr (4, a2) expr (4, a3) end; if prec' < prec then fprintf p ")@]" else fprintf p "@]" @@ -125,8 +123,6 @@ let rec print_stmt p s = fprintf p "@[<hv 2>%a =@ %a;@]" print_expr e1 print_expr e2 | Sset(id, e2) -> fprintf p "@[<hv 2>%s =@ %a;@]" (temp_name id) print_expr e2 - | Svolread(id, e2) -> - fprintf p "@[<hv 2>%s =@ %a; /*volatile*/@]" (temp_name id) print_expr e2 | Scall(None, e1, el) -> fprintf p "@[<hv 2>%a@,(@[<hov 0>%a@]);@]" print_expr e1 @@ -136,6 +132,15 @@ let rec print_stmt p s = (temp_name id) print_expr e1 print_expr_list (true, el) + | Sbuiltin(None, ef, tyargs, el) -> + fprintf p "@[<hv 2>builtin %s@,(@[<hov 0>%a@]);@]" + (name_of_external ef) + print_expr_list (true, el) + | Sbuiltin(Some id, ef, tyargs, el) -> + fprintf p "@[<hv 2>%s =@ builtin %s@,(@[<hov 0>%a@]);@]" + (temp_name id) + (name_of_external ef) + print_expr_list (true, el) | Ssequence(Sskip, s2) -> print_stmt p s2 | Ssequence(s1, Sskip) -> @@ -155,19 +160,13 @@ let rec print_stmt p s = print_expr e print_stmt s1 print_stmt s2 - | Swhile(e, s) -> - fprintf p "@[<v 2>while (%a) {@ %a@;<0 -2>}@]" - print_expr e - print_stmt s - | Sdowhile(e, s) -> - fprintf p "@[<v 2>do {@ %a@;<0 -2>} while(%a);@]" - print_stmt s - print_expr e - | Sfor'(e, s_iter, s_body) -> - fprintf p "@[<v 2>for (@[<hv 0>;@ %a;@ %a) {@]@ %a@;<0 -2>}@]" - print_expr e - print_stmt_for s_iter - print_stmt s_body + | Sloop(s1, Sskip) -> + fprintf p "@[<v 2>while (1) {@ %a@;<0 -2>}@]" + print_stmt s1 + | Sloop(s1, s2) -> + fprintf p "@[<v 2>for (@[<hv 0>;@ 1;@ %a) {@]@ %a@;<0 -2>}@]" + print_stmt_for s2 + print_stmt s1 | Sbreak -> fprintf p "break;" | Scontinue -> @@ -220,6 +219,15 @@ and print_stmt_for p s = (temp_name id) print_expr e1 print_expr_list (true, el) + | Sbuiltin(None, ef, tyargs, el) -> + fprintf p "@[<hv 2>builtin %s@,(@[<hov 0>%a@]);@]" + (name_of_external ef) + print_expr_list (true, el) + | Sbuiltin(Some id, ef, tyargs, el) -> + fprintf p "@[<hv 2>%s =@ builtin %s@,(@[<hov 0>%a@]);@]" + (temp_name id) + (name_of_external ef) + print_expr_list (true, el) | _ -> fprintf p "({ %a })" print_stmt s @@ -265,8 +273,6 @@ let rec collect_expr e = | Eunop(_, r, _) -> collect_expr r | Ebinop(_, r1, r2, _) -> collect_expr r1; collect_expr r2 | Ecast(r, _) -> collect_expr r - | Econdition(r1, r2, r3, _) -> - collect_expr r1; collect_expr r2; collect_expr r3 let rec collect_exprlist = function | [] -> () @@ -276,14 +282,11 @@ let rec collect_stmt = function | Sskip -> () | Sassign(e1, e2) -> collect_expr e1; collect_expr e2 | Sset(id, e2) -> collect_expr e2 - | Svolread(id, e2) -> collect_expr e2 | Scall(optid, e1, el) -> collect_expr e1; collect_exprlist el + | Sbuiltin(optid, ef, tyargs, el) -> collect_exprlist el | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2 | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2 - | Swhile(e, s) -> collect_expr e; collect_stmt s - | Sdowhile(e, s) -> collect_stmt s; collect_expr e - | Sfor'(e, s_iter, s_body) -> - collect_expr e; collect_stmt s_iter; collect_stmt s_body + | Sloop(s1, s2) -> collect_stmt s1; collect_stmt s2 | Sbreak -> () | Scontinue -> () | Sswitch(e, cases) -> collect_expr e; collect_cases cases |