diff options
Diffstat (limited to 'backend/Cminor.v')
| -rw-r--r-- | backend/Cminor.v | 6 |
1 files changed, 3 insertions, 3 deletions
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. |