diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-03-27 11:48:04 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-03-27 11:48:04 +0100 |
| commit | ecbecdd399d0d685ffed2024e864dc4aaccdfbf6 (patch) | |
| tree | 5546d9139c4c1586355f9c6b8e43cc8b1c812042 /cfrontend/Cexec.v | |
| parent | 4622f49fd089ae47d0c853343cb0a05f986c962a (diff) | |
| download | compcert-kvx-ecbecdd399d0d685ffed2024e864dc4aaccdfbf6.tar.gz compcert-kvx-ecbecdd399d0d685ffed2024e864dc4aaccdfbf6.zip | |
Extended arguments to annotations, continued:
- Simplifications in RTLgen.
- Updated Cexec.
Diffstat (limited to 'cfrontend/Cexec.v')
| -rw-r--r-- | cfrontend/Cexec.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index ed67286f..66427b76 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -513,10 +513,10 @@ Definition do_ef_memcpy (sz al: Z) | _ => None end. -Definition do_ef_annot (text: ident) (targs: list annot_arg) +Definition do_ef_annot (text: ident) (targs: list typ) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - do args <- list_eventval_of_val vargs (annot_args_typ targs); - Some(w, Event_annot text (annot_eventvals targs args) :: E0, Vundef, m). + do args <- list_eventval_of_val vargs targs; + Some(w, Event_annot text 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) := |