aboutsummaryrefslogtreecommitdiffstats
path: root/backend/RTLgenaux.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-03-15 15:07:47 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2016-03-15 15:07:47 +0100
commit272a5b812b72f4c3e409ccdbeaf3476d95c4b552 (patch)
tree6a8d5e75a11860b69522cef3b512b1ef5effb438 /backend/RTLgenaux.ml
parent2185164c1845c30ebd4118ed5bc8d339b16663a9 (diff)
downloadcompcert-kvx-272a5b812b72f4c3e409ccdbeaf3476d95c4b552.tar.gz
compcert-kvx-272a5b812b72f4c3e409ccdbeaf3476d95c4b552.zip
Deactivate warning 27 and added back removed code.
The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
Diffstat (limited to 'backend/RTLgenaux.ml')
-rw-r--r--backend/RTLgenaux.ml40
1 files changed, 20 insertions, 20 deletions
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml
index fdf41897..e39d3b56 100644
--- a/backend/RTLgenaux.ml
+++ b/backend/RTLgenaux.ml
@@ -26,22 +26,22 @@ open CminorSel
putting the bigger of the two branches in fall-through position. *)
let rec size_expr = function
- | Evar _ -> 0
- | Eop(_, args) -> 1 + size_exprs args
- | Eload(_, _, args) -> 1 + size_exprs args
+ | Evar id -> 0
+ | Eop(op, args) -> 1 + size_exprs args
+ | Eload(chunk, addr, args) -> 1 + size_exprs args
| Econdition(ce, e1, e2) ->
1 + size_condexpr ce + max (size_expr e1) (size_expr e2)
| Elet(e1, e2) -> size_expr e1 + size_expr e2
- | Eletvar _ -> 0
- | Ebuiltin(_, el) -> 2 + size_exprs el
- | Eexternal(_, _, el) -> 5 + size_exprs el
+ | Eletvar n -> 0
+ | Ebuiltin(ef, el) -> 2 + size_exprs el
+ | Eexternal(id, sg, el) -> 5 + size_exprs el
and size_exprs = function
| Enil -> 0
| Econs(e1, el) -> size_expr e1 + size_exprs el
and size_condexpr = function
- | CEcond(_, args) -> size_exprs args
+ | CEcond(c, args) -> size_exprs args
| CEcondition(c1, c2, c3) ->
1 + size_condexpr c1 + size_condexpr c2 + size_condexpr c3
| CElet(a, c) ->
@@ -52,8 +52,8 @@ let size_exprlist al = List.fold_right (fun a s -> size_expr a + s) al 0
let size_builtin_args al = size_exprlist (params_of_builtin_args al)
let rec size_exitexpr = function
- | XEexit _ -> 0
- | XEjumptable(arg, _) -> 2 + size_expr arg
+ | XEexit n -> 0
+ | XEjumptable(arg, tbl) -> 2 + size_expr arg
| XEcondition(c1, c2, c3) ->
1 + size_condexpr c1 + size_exitexpr c2 + size_exitexpr c3
| XElet(a, c) ->
@@ -61,34 +61,34 @@ let rec size_exitexpr = function
let rec length_exprs = function
| Enil -> 0
- | Econs(_, el) -> 1 + length_exprs el
+ | Econs(e1, el) -> 1 + length_exprs el
let size_eos = function
| Coq_inl e -> size_expr e
- | Coq_inr _ -> 0
+ | Coq_inr id -> 0
let rec size_stmt = function
| Sskip -> 0
- | Sassign(_, a) -> size_expr a
- | Sstore(_, _, args, src) -> 1 + size_exprs args + size_expr src
- | Scall(_, _, eos, args) ->
+ | Sassign(id, a) -> size_expr a
+ | Sstore(chunk, addr, args, src) -> 1 + size_exprs args + size_expr src
+ | Scall(optid, sg, eos, args) ->
3 + size_eos eos + size_exprs args + length_exprs args
- | Stailcall(_, eos, args) ->
+ | Stailcall(sg, eos, args) ->
3 + size_eos eos + size_exprs args + length_exprs args
| Sbuiltin(_, (EF_annot _ | EF_debug _), _) -> 0
- | Sbuiltin(_, _, args) -> 1 + size_builtin_args args
+ | Sbuiltin(optid, ef, args) -> 1 + size_builtin_args args
| Sseq(s1, s2) -> size_stmt s1 + size_stmt s2
| Sifthenelse(ce, s1, s2) ->
size_condexpr ce + max (size_stmt s1) (size_stmt s2)
| Sloop s -> 1 + 4 * size_stmt s
| Sblock s -> size_stmt s
- | Sexit _ -> 1
+ | Sexit n -> 1
| Sswitch xe -> size_exitexpr xe
| Sreturn None -> 2
| Sreturn (Some arg) -> 2 + size_expr arg
- | Slabel(_, s) -> size_stmt s
- | Sgoto _ -> 1
+ | Slabel(lbl, s) -> size_stmt s
+ | Sgoto lbl -> 1
-let more_likely (_: condexpr) (ifso: stmt) (ifnot: stmt) =
+let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) =
size_stmt ifso > size_stmt ifnot