diff options
Diffstat (limited to 'backend/Linear.v')
-rw-r--r-- | backend/Linear.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Linear.v b/backend/Linear.v index 3c524368..56d1eb99 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. |