aboutsummaryrefslogtreecommitdiffstats
path: root/backend/PrintXTL.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/PrintXTL.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/PrintXTL.ml')
-rw-r--r--backend/PrintXTL.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index 1bee1e15..31273f97 100644
--- a/backend/PrintXTL.ml
+++ b/backend/PrintXTL.ml
@@ -67,8 +67,8 @@ let ros pp = function
let liveset pp lv =
fprintf pp "{";
- VSet.iter (function V(r, _) -> fprintf pp " x%d" (P.to_int r)
- | L _ -> ())
+ VSet.iter (function V(r, ty) -> fprintf pp " x%d" (P.to_int r)
+ | L l -> ())
lv;
fprintf pp " }"
@@ -93,9 +93,9 @@ let print_instruction pp succ = function
| Xstore(chunk, addr, args, src) ->
fprintf pp "%s[%a] = %a"
(name_of_chunk chunk) (print_addressing var) (addr, args) var src
- | Xcall(_, fn, args, res) ->
+ | Xcall(sg, fn, args, res) ->
fprintf pp "%a = call %a(%a)" vars res ros fn vars args
- | Xtailcall(_, fn, args) ->
+ | Xtailcall(sg, fn, args) ->
fprintf pp "tailcall %a(%a)" ros fn vars args
| Xbuiltin(ef, args, res) ->
fprintf pp "%a = %s(%a)"