diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-24 09:01:28 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-24 09:01:28 +0000 |
| commit | 202bc495442a1a8fa184b73ac0063bdbbbcdf846 (patch) | |
| tree | 46c6920201b823bf47252bc52864b0bf60f3233e /cfrontend | |
| parent | f774d5f2d604f747e72e2d3bb56cc3f90090e2dd (diff) | |
Constant propagation within __builtin_annot.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 6 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 9 |
2 files changed, 9 insertions, 6 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 4233af9..f34c396 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -511,8 +511,10 @@ let rec convertExpr env e = begin match args with | {edesc = C.EConst(CStr txt)} :: args1 -> let targs1 = convertTypList env (List.map (fun e -> e.etyp) args1) in - Ebuiltin(EF_annot(intern_string txt, typlist_of_typelist targs1), - targs1, convertExprList env args1, ty) + Ebuiltin( + EF_annot(intern_string txt, + List.map (fun t -> AA_arg t) (typlist_of_typelist targs1)), + targs1, convertExprList env args1, ty) | _ -> error "ill-formed __builtin_annot (first argument must be string literal)"; ezero diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index ded6b72..c638259 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -478,10 +478,10 @@ Definition do_ef_memcpy (sz al: Z) | _ => None end. -Definition do_ef_annot (text: ident) (targs: list typ) +Definition do_ef_annot (text: ident) (targs: list annot_arg) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - do args <- list_eventval_of_val vargs targs; - Some(w, Event_annot text args :: E0, Vundef, m). + do args <- list_eventval_of_val vargs (annot_args_typ targs); + Some(w, Event_annot text (annot_eventvals targs args) :: E0, Vundef, m). Definition do_ef_annot_val (text: ident) (targ: typ) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := @@ -578,7 +578,8 @@ Proof with try congruence. econstructor. constructor; eauto. constructor. (* EF_inline_asm *) unfold do_ef_annot. destruct vargs; simpl... mydestr. - split. constructor. constructor. + split. change (Event_annot text nil) with (Event_annot text (annot_eventvals nil nil)). + constructor. constructor. econstructor. constructor; eauto. constructor. Qed. |