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 /backend/PrintCminor.ml | |
| parent | 261ef24f7fd2ef443f73c468b9b1fa496371f3bf (diff) | |
| download | compcert-kvx-f7693b3d897b90fd3bc2533be002dc0bdcd9f6c2.tar.gz compcert-kvx-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 'backend/PrintCminor.ml')
| -rw-r--r-- | backend/PrintCminor.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 66b579e7..858ef219 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -40,7 +40,6 @@ let rec precedence = function | Ebinop(Oxor, _, _) -> (7, LtoR) | Ebinop(Oor, _, _) -> (6, LtoR) | Eload _ -> (15, RtoL) - | Econdition _ -> (3, RtoL) (* Naming idents. We assume idents are encoded as in Cminorgen. *) @@ -58,8 +57,6 @@ let name_of_unop = function | Ocast16unsigned -> "int16u" | Ocast16signed -> "int16s" | Onegint -> "-" - | Oboolval -> "(_Bool)" - | Onotbool -> "!" | Onotint -> "~" | Onegf -> "-f" | Oabsf -> "absf" @@ -141,8 +138,6 @@ let rec expr p (prec, e) = expr (prec1, a1) (name_of_binop op) expr (prec2, a2) | Eload(chunk, a1) -> fprintf p "%s[%a]" (name_of_chunk chunk) expr (0, 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 "@]" |