summaryrefslogtreecommitdiff
path: root/backend
diff options
context:
space:
mode:
Diffstat (limited to 'backend')
-rw-r--r--backend/CMparser.mly4
-rw-r--r--backend/Cminor.v6
-rw-r--r--backend/CminorSel.v2
-rw-r--r--backend/LTL.v4
-rw-r--r--backend/Linear.v4
-rw-r--r--backend/Mach.v2
-rw-r--r--backend/PrintCminor.ml13
-rw-r--r--backend/RTL.v2
-rw-r--r--backend/SelectLong.vp14
9 files changed, 26 insertions, 25 deletions
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index b28578e..5d93b84 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -490,9 +490,9 @@ proc:
signature:
type_
- { {sig_args = []; sig_res = Some $1} }
+ { {sig_args = []; sig_res = Some $1; sig_cc = cc_default} }
| VOID
- { {sig_args = []; sig_res = None} }
+ { {sig_args = []; sig_res = None; sig_cc = cc_default} }
| type_ MINUSGREATER signature
{ let s = $3 in {s with sig_args = $1 :: s.sig_args} }
;
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 9f7244b..c12c6fc 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -532,7 +532,7 @@ Inductive initial_state (p: program): state -> Prop :=
Genv.init_mem p = Some m0 ->
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
- funsig f = mksignature nil (Some Tint) ->
+ funsig f = signature_main ->
initial_state p (Callstate f nil Kstop m0).
(** A final state is a [Returnstate] with an empty continuation. *)
@@ -811,7 +811,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
Genv.init_mem p = Some m0 ->
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
- funsig f = mksignature nil (Some Tint) ->
+ funsig f = signature_main ->
eval_funcall ge m0 f nil t m (Vint r) ->
bigstep_program_terminates p t r.
@@ -822,7 +822,7 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
Genv.init_mem p = Some m0 ->
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
- funsig f = mksignature nil (Some Tint) ->
+ funsig f = signature_main ->
evalinf_funcall ge m0 f nil t ->
bigstep_program_diverges p t.
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index c80f424..db414a2 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -390,7 +390,7 @@ Inductive initial_state (p: program): state -> Prop :=
Genv.init_mem p = Some m0 ->
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
- funsig f = mksignature nil (Some Tint) ->
+ funsig f = signature_main ->
initial_state p (Callstate f nil Kstop m0).
Inductive final_state: state -> int -> Prop :=
diff --git a/backend/LTL.v b/backend/LTL.v
index e60600a..dd79c8e 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -295,12 +295,12 @@ Inductive initial_state (p: program): state -> Prop :=
Genv.init_mem p = Some m0 ->
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
- funsig f = mksignature nil (Some Tint) ->
+ funsig f = signature_main ->
initial_state p (Callstate nil f (Locmap.init Vundef) m0).
Inductive final_state: state -> int -> Prop :=
| final_state_intro: forall rs m r retcode,
- loc_result (mksignature nil (Some Tint)) = r :: nil ->
+ loc_result signature_main = r :: nil ->
rs (R r) = Vint retcode ->
final_state (Returnstate nil rs m) retcode.
diff --git a/backend/Linear.v b/backend/Linear.v
index 3c52436..56d1eb9 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -269,12 +269,12 @@ Inductive initial_state (p: program): state -> Prop :=
Genv.init_mem p = Some m0 ->
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
- funsig f = mksignature nil (Some Tint) ->
+ funsig f = signature_main ->
initial_state p (Callstate nil f (Locmap.init Vundef) m0).
Inductive final_state: state -> int -> Prop :=
| final_state_intro: forall rs m r retcode,
- loc_result (mksignature nil (Some Tint)) = r :: nil ->
+ loc_result signature_main = r :: nil ->
rs (R r) = Vint retcode ->
final_state (Returnstate nil rs m) retcode.
diff --git a/backend/Mach.v b/backend/Mach.v
index f0fb56a..ff72a82 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -427,7 +427,7 @@ Inductive initial_state (p: program): state -> Prop :=
Inductive final_state: state -> int -> Prop :=
| final_state_intro: forall rs m r retcode,
- loc_result (mksignature nil (Some Tint)) = r :: nil ->
+ loc_result signature_main = r :: nil ->
rs r = Vint retcode ->
final_state (Returnstate nil rs m) retcode.
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 33c38f5..4c53c5e 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -172,12 +172,13 @@ let name_of_type = function
| Tlong -> "long"
| Tsingle -> "single"
-let rec print_sig p = function
- | {sig_args = []; sig_res = None} -> fprintf p "void"
- | {sig_args = []; sig_res = Some ty} -> fprintf p "%s" (name_of_type ty)
- | {sig_args = t1 :: tl; sig_res = tres} ->
- fprintf p "%s ->@ " (name_of_type t1);
- print_sig p {sig_args = tl; sig_res = tres}
+let print_sig p sg =
+ List.iter
+ (fun t -> fprintf p "%s ->@ " (name_of_type t))
+ sg.sig_args;
+ match sg.sig_res with
+ | None -> fprintf p "void"
+ | Some ty -> fprintf p "%s" (name_of_type ty)
let rec just_skips s =
match s with
diff --git a/backend/RTL.v b/backend/RTL.v
index b2e1e89..045250d 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -331,7 +331,7 @@ Inductive initial_state (p: program): state -> Prop :=
Genv.init_mem p = Some m0 ->
Genv.find_symbol ge p.(prog_main) = Some b ->
Genv.find_funct_ptr ge b = Some f ->
- funsig f = mksignature nil (Some Tint) ->
+ funsig f = signature_main ->
initial_state p (Callstate nil f nil m0).
(** A final state is a [Returnstate] with an empty call stack. *)
diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp
index 76cc79d..09f29af 100644
--- a/backend/SelectLong.vp
+++ b/backend/SelectLong.vp
@@ -46,13 +46,13 @@ Record helper_functions : Type := mk_helper_functions {
i64_sar: ident (**r shift right signed *)
}.
-Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong).
-Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat).
-Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle).
-Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong).
-Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong).
-Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong).
-Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong).
+Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default.
+Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default.
+Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default.
+Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default.
+Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default.
+Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default.
+Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default.
Section SELECT.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 23:59:52 +0000