diff --git a/src/plugins/variadic/classify.ml b/src/plugins/variadic/classify.ml index df2f128c752d019f362cceca9f6735e860cb6a23..5d492765d0ddb470f7c437da4418ae2af661e02e 100644 --- a/src/plugins/variadic/classify.ml +++ b/src/plugins/variadic/classify.ml @@ -148,6 +148,7 @@ let classify_std env vi = match vi.vname with (* stropts.h *) | "ioctl" -> mk_overload env ["__va_ioctl_void" ; "__va_ioctl_int" ; "__va_ioctl_ptr"] + | n when Extlib.string_prefix "__sync_" n -> Misc | n when Cil_builtins.Builtin_functions.mem n -> Builtin (* Anything else *) | _ -> Unknown diff --git a/src/plugins/variadic/translate.ml b/src/plugins/variadic/translate.ml index b2bbd04dbb1302f8de40b034909dbbebf1b1b46f..bf32abcdf50d6cae2a3d62bd75df158e77d48e43 100644 --- a/src/plugins/variadic/translate.ml +++ b/src/plugins/variadic/translate.ml @@ -54,8 +54,7 @@ let translate_variadics (file : file) = method! vglob glob = begin match glob with - | GFunDecl(_, vi, _) | GFun ({svar = vi}, _) - when not (is_framac_builtin vi) -> + | GFunDecl(_, vi, _) | GFun ({svar = vi}, _) -> if not (Table.mem classification vi) then begin let vf = Classify.classify env vi in Option.iter (Table.add classification vi) vf @@ -88,16 +87,14 @@ let translate_variadics (file : file) = (* Translate types and signatures *) method! vglob glob = begin match glob with - | GFunDecl(_, vi, _) when is_framac_builtin vi -> - if Classify.classify env vi <> None then begin - Self.result ~level:2 ~current:true - "Variadic builtin %s left untransformed." vi.vname; - end; - Cil.SkipChildren - | GFunDecl(_, vi, _) -> - if Table.mem classification vi then - Generic.add_vpar vi; + (match Table.find_opt classification vi with + | None -> () + | Some { vf_class = Builtin } -> + Self.result ~level:2 ~current:true + "Variadic builtin %s left untransformed." vi.vname; + | Some _ -> + Generic.add_vpar vi); Cil.DoChildren | GFun ({svar = vi} as fundec, _) ->