diff options
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 3 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 6 |
2 files changed, 4 insertions, 5 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 4cb4ded6..fd10efb4 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -737,8 +737,7 @@ let rec convertExpr env e = | {edesc = C.EConst(CStr txt)} :: args1 -> let targs1 = convertTypArgs env [] args1 in Ebuiltin( - EF_annot(intern_string txt, - List.map (fun t -> AA_arg t) (typlist_of_typelist targs1)), + EF_annot(intern_string txt, typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> error "ill-formed __builtin_annot (first argument must be string literal)"; diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 52e9eaac..7c00ab47 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) := |