diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-14 14:00:57 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-14 14:00:57 +0000 |
commit | 5fccbcb628c5282cf1b13077d5eeccf497d58c38 (patch) | |
tree | a39fa4c2ba74de33ec3a2a48b2309175ab65a271 /cfrontend/Clight.v | |
parent | 0f5087bea45be49e105727d6cee4194598474fee (diff) | |
download | compcert-5fccbcb628c5282cf1b13077d5eeccf497d58c38.tar.gz compcert-5fccbcb628c5282cf1b13077d5eeccf497d58c38.zip |
Fix treatment of function pointers at function calls in the CompCert C and Clight semantics
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1680 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Clight.v')
-rw-r--r-- | cfrontend/Clight.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 50be0393..da8f668f 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -433,11 +433,11 @@ Inductive step: state -> trace -> state -> Prop := E0 (State f Sskip k e (PTree.set id v le) m) | step_call: forall f optid a al k e le m tyargs tyres vf vargs fd, - typeof a = Tfunction tyargs tyres -> + classify_fun (typeof a) = fun_case_f tyargs tyres -> eval_expr e le m a vf -> eval_exprlist e le m al tyargs vargs -> Genv.find_funct ge vf = Some fd -> - type_of_fundef fd = typeof a -> + type_of_fundef fd = Tfunction tyargs tyres -> step (State f (Scall optid a al) k e le m) E0 (Callstate fd vargs (Kcall optid f e le k) m) @@ -643,20 +643,20 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> exec_stmt e le m (Sset id a) E0 (PTree.set id v le) m Out_normal | exec_Scall_none: forall e le m a al tyargs tyres vf vargs f t m' vres, - typeof a = Tfunction tyargs tyres -> + classify_fun (typeof a) = fun_case_f tyargs tyres -> eval_expr e le m a vf -> eval_exprlist e le m al tyargs vargs -> Genv.find_funct ge vf = Some f -> - type_of_fundef f = typeof a -> + type_of_fundef f = Tfunction tyargs tyres -> eval_funcall m f vargs t m' vres -> exec_stmt e le m (Scall None a al) t le m' Out_normal | exec_Scall_some: forall e le m id a al tyargs tyres vf vargs f t m' vres, - typeof a = Tfunction tyargs tyres -> + classify_fun (typeof a) = fun_case_f tyargs tyres -> eval_expr e le m a vf -> eval_exprlist e le m al tyargs vargs -> Genv.find_funct ge vf = Some f -> - type_of_fundef f = typeof a -> + type_of_fundef f = Tfunction tyargs tyres -> eval_funcall m f vargs t m' vres -> exec_stmt e le m (Scall (Some id) a al) t (PTree.set id vres le) m' Out_normal @@ -792,19 +792,19 @@ Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Prop := | execinf_Scall_none: forall e le m a al vf tyargs tyres vargs f t, - typeof a = Tfunction tyargs tyres -> + classify_fun (typeof a) = fun_case_f tyargs tyres -> eval_expr e le m a vf -> eval_exprlist e le m al tyargs vargs -> Genv.find_funct ge vf = Some f -> - type_of_fundef f = typeof a -> + type_of_fundef f = Tfunction tyargs tyres -> evalinf_funcall m f vargs t -> execinf_stmt e le m (Scall None a al) t | execinf_Scall_some: forall e le m id a al vf tyargs tyres vargs f t, - typeof a = Tfunction tyargs tyres -> + classify_fun (typeof a) = fun_case_f tyargs tyres -> eval_expr e le m a vf -> eval_exprlist e le m al tyargs vargs -> Genv.find_funct ge vf = Some f -> - type_of_fundef f = typeof a -> + type_of_fundef f = Tfunction tyargs tyres -> evalinf_funcall m f vargs t -> execinf_stmt e le m (Scall (Some id) a al) t | execinf_Sseq_1: forall e le m s1 s2 t, |