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