From 9644abd733c93723d4d11ab8c58a27f888d6630c Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Thu, 7 Jan 2021 18:43:30 +0100 Subject: [PATCH] [variadic] translates __sync family --- src/plugins/variadic/classify.ml | 1 + src/plugins/variadic/translate.ml | 19 ++++++++----------- 2 files changed, 9 insertions(+), 11 deletions(-) diff --git a/src/plugins/variadic/classify.ml b/src/plugins/variadic/classify.ml index df2f128c752..5d492765d0d 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 b2bbd04dbb1..bf32abcdf50 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, _) -> -- GitLab