aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Asmexpandaux.ml
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2018-11-26 17:35:31 +0100
committerCyril SIX <cyril.six@kalray.eu>2018-11-26 17:35:31 +0100
commit5631ccb7c416bb7ecbe7920cb432a78436c0a7ac (patch)
treec84dfc9edea4d1aaf48985a229dddb811cbc3ffa /backend/Asmexpandaux.ml
parent3d38bf85c8ac3a83fe7aaeb5e01bb9a8403e6a60 (diff)
downloadcompcert-kvx-5631ccb7c416bb7ecbe7920cb432a78436c0a7ac.tar.gz
compcert-kvx-5631ccb7c416bb7ecbe7920cb432a78436c0a7ac.zip
BROKEN - works for x86, not for k1 anymore
Diffstat (limited to 'backend/Asmexpandaux.ml')
-rw-r--r--backend/Asmexpandaux.ml8
1 files changed, 3 insertions, 5 deletions
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index 0f666a65..f5c76925 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -26,9 +26,7 @@ let emit i = current_code := i :: !current_code
(* Generation of fresh labels *)
-(** dummy_funtion is now defined in Asm.v *)
-(* let dummy_function = { fn_code = []; fn_sig = signature_main } *)
-
+let dummy_function = { fn_code = []; fn_sig = signature_main }
let current_function = ref dummy_function
let next_label = ref (None: label option)
@@ -122,7 +120,7 @@ let expand_debug id sp preg simple l =
begin
match kind with
| 1->
- emit i; aux lbl scopes rest
+ emit i;aux lbl scopes rest
| 2 ->
aux lbl scopes rest
| 3 ->
@@ -163,7 +161,7 @@ let expand_debug id sp preg simple l =
| i::rest -> simple i; aux None scopes rest in
(* We need to move all closing debug annotations before the last real statement *)
let rec move_debug acc bcc = function
- | (Pbuiltin(EF_debug (kind,_,_),_,_)) as i::rest ->
+ | (Pbuiltin(EF_debug (kind,_,_),_,_) as i)::rest ->
let kind = (P.to_int kind) in
if kind = 1 then
move_debug acc (i::bcc) rest (* Do not move debug line *)