diff options
Diffstat (limited to 'backend/RTL.v')
-rw-r--r-- | backend/RTL.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/RTL.v b/backend/RTL.v index b2e1e89c..045250da 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. *) |