diff options
Diffstat (limited to 'cfrontend/Cstrategy.v')
| -rw-r--r-- | cfrontend/Cstrategy.v | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 7988dfa..b1fbebe 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -359,13 +359,13 @@ Inductive estep: state -> trace -> state -> Prop := estep (ExprState f (C (Eparen r ty)) k e m) E0 (ExprState f (C (Eval v ty)) k e m) - | step_call: forall f C rf rargs ty k e m targs tres vf vargs fd, + | step_call: forall f C rf rargs ty k e m targs tres cconv vf vargs fd, leftcontext RV RV C -> - classify_fun (typeof rf) = fun_case_f targs tres -> + classify_fun (typeof rf) = fun_case_f targs tres cconv -> eval_simple_rvalue e m rf vf -> eval_simple_list e m rargs targs vargs -> Genv.find_funct ge vf = Some fd -> - type_of_fundef fd = Tfunction targs tres -> + type_of_fundef fd = Tfunction targs tres cconv -> estep (ExprState f (C (Ecall rf rargs ty)) k e m) E0 (Callstate fd vargs (Kcall f e C ty k) m) @@ -562,11 +562,11 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := exists v, sem_cast v1 ty1 ty = Some v | Ecall (Eval vf tyf) rargs ty => exprlist_all_values rargs -> - exists tyargs, exists tyres, exists fd, exists vl, - classify_fun tyf = fun_case_f tyargs tyres + exists tyargs tyres cconv fd vl, + classify_fun tyf = fun_case_f tyargs tyres cconv /\ Genv.find_funct ge vf = Some fd /\ cast_arguments rargs tyargs vl - /\ type_of_fundef fd = Tfunction tyargs tyres + /\ type_of_fundef fd = Tfunction tyargs tyres cconv | Ebuiltin ef tyargs rargs ty => exprlist_all_values rargs -> exists vargs, exists t, exists vres, exists m', @@ -610,7 +610,7 @@ Lemma callred_invert: invert_expr_prop r m. Proof. intros. inv H. simpl. - intros. exists tyargs; exists tyres; exists fd; exists args; auto. + intros. exists tyargs, tyres, cconv, fd, args; auto. Qed. Scheme context_ind2 := Minimality for context Sort Prop @@ -1369,7 +1369,7 @@ Proof. eapply safe_steps. eexact S1. apply (eval_simple_list_steps f k e m rargs vl E2 C'); auto. simpl. intros X. exploit X. eapply rval_list_all_values. - intros [tyargs [tyres [fd [vargs [P [Q [U V]]]]]]]. + intros [tyargs [tyres [cconv [fd [vargs [P [Q [U V]]]]]]]]. econstructor; econstructor; eapply step_call; eauto. eapply can_eval_simple_list; eauto. (* builtin *) pose (C' := fun x => C(Ebuiltin ef tyargs x ty)). @@ -1756,13 +1756,13 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := ty = typeof r2 -> eval_expr e m RV (Ecomma r1 r2 ty) (t1**t2) m2 r2' | eval_call: forall e m rf rargs ty t1 m1 rf' t2 m2 rargs' vf vargs - targs tres fd t3 m3 vres, + targs tres cconv fd t3 m3 vres, eval_expr e m RV rf t1 m1 rf' -> eval_exprlist e m1 rargs t2 m2 rargs' -> eval_simple_rvalue ge e m2 rf' vf -> eval_simple_list ge e m2 rargs' targs vargs -> - classify_fun (typeof rf) = fun_case_f targs tres -> + classify_fun (typeof rf) = fun_case_f targs tres cconv -> Genv.find_funct ge vf = Some fd -> - type_of_fundef fd = Tfunction targs tres -> + type_of_fundef fd = Tfunction targs tres cconv -> eval_funcall m2 fd vargs t3 m3 vres -> eval_expr e m RV (Ecall rf rargs ty) (t1**t2**t3) m3 (Eval vres ty) @@ -1901,9 +1901,9 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := outcome_result_value out f.(fn_return) vres -> Mem.free_list m3 (blocks_of_env e) = Some m4 -> eval_funcall m (Internal f) vargs t m4 vres - | eval_funcall_external: forall m ef targs tres vargs t vres m', + | eval_funcall_external: forall m ef targs tres cconv vargs t vres m', external_call ef ge vargs m t vres m' -> - eval_funcall m (External ef targs tres) vargs t m' vres. + eval_funcall m (External ef targs tres cconv) vargs t m' vres. Scheme eval_expression_ind5 := Minimality for eval_expression Sort Prop with eval_expr_ind5 := Minimality for eval_expr Sort Prop @@ -1999,13 +1999,13 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := evalinf_exprlist e m1 a2 t2 -> evalinf_expr e m RV (Ecall a1 a2 ty) (t1 *** t2) | evalinf_call: forall e m rf rargs ty t1 m1 rf' t2 m2 rargs' vf vargs - targs tres fd t3, + targs tres cconv fd t3, eval_expr e m RV rf t1 m1 rf' -> eval_exprlist e m1 rargs t2 m2 rargs' -> eval_simple_rvalue ge e m2 rf' vf -> eval_simple_list ge e m2 rargs' targs vargs -> - classify_fun (typeof rf) = fun_case_f targs tres -> + classify_fun (typeof rf) = fun_case_f targs tres cconv -> Genv.find_funct ge vf = Some fd -> - type_of_fundef fd = Tfunction targs tres -> + type_of_fundef fd = Tfunction targs tres cconv -> evalinf_funcall m2 fd vargs t3 -> evalinf_expr e m RV (Ecall rf rargs ty) (t1***t2***t3) @@ -3034,7 +3034,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 -> - type_of_fundef f = Tfunction Tnil type_int32s -> + type_of_fundef f = Tfunction Tnil type_int32s cc_default -> eval_funcall ge m0 f nil t m1 (Vint r) -> bigstep_program_terminates p t r. @@ -3044,7 +3044,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 -> - type_of_fundef f = Tfunction Tnil type_int32s -> + type_of_fundef f = Tfunction Tnil type_int32s cc_default -> evalinf_funcall ge m0 f nil t -> bigstep_program_diverges p t. |