diff --git a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
index 1dc6823676ef7ee36ab009e4916d0cfc77a8ea33..a1dde62c222737a8ba75bf5599a8fc7c642b7925 100644
--- a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
@@ -1,6 +1,4 @@
[kernel] Parsing tests/ya/serial.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/ya/serial.c:79: Warning:
- Calling undeclared function Frama_C_show_aorai_state. Old style K&R code?
[aorai] Welcome to the Aorai plugin
[kernel:annot:missing-spec] tests/ya/serial.c:43: Warning:
Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
@@ -299,7 +297,7 @@
100% of the logical properties reached have been proven.
----------------------------------------------------------------------------
[kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
-[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:176: Warning:
+[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:174: Warning:
Calling undeclared function Frama_C_interval. Old style K&R code?
/* Generated by Frama-C */
enum aorai_States {
@@ -338,13 +336,11 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
+/* compiler builtin:
+ void Frama_C_show_aorai_state(...); */
int volatile indefinitely;
int buffer[5];
int n = 0;
-/*@ assigns \result;
- assigns \result \from \nothing; */
-extern int Frama_C_show_aorai_state(void);
-
/*@ ghost enum aorai_ListOper aorai_CurOperation; */
/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int aorai_CurStates = Wait1; */
diff --git a/src/plugins/variadic/classify.ml b/src/plugins/variadic/classify.ml
index 5d492765d0ddb470f7c437da4418ae2af661e02e..80b9c73dfc85db1828aacf1c9e530c078134c780 100644
--- a/src/plugins/variadic/classify.ml
+++ b/src/plugins/variadic/classify.ml
@@ -110,6 +110,20 @@ let mk_format_fun vi f_kind f_buffer ~format_pos =
(* Classification *)
(* ************************************************************************ *)
+let is_frama_c_builtin name =
+ Ast_info.is_frama_c_builtin name ||
+ Cil_builtins.Builtin_functions.mem name ||
+ Extlib.string_prefix "__FRAMAC_" name (* Mthread prefixes *)
+
+let va_builtins = [
+ "__builtin_va_start";
+ "__builtin_va_copy";
+ "__builtin_va_arg";
+ "__builtin_va_end";
+]
+
+let is_va_builtin s = List.mem s va_builtins
+
let classify_std env vi = match vi.vname with
(* fcntl.h - Overloads of functions *)
| "fcntl" -> mk_overload env
@@ -149,7 +163,8 @@ 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
+ | n when is_va_builtin n -> Misc
+ | n when is_frama_c_builtin n -> Builtin
(* Anything else *)
| _ -> Unknown
diff --git a/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
index a5caa303321a2c8a59eeca0aa1e0fd1d70baad98..bf189af5926715a5665d71211f84b792dbffd641 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
@@ -2,6 +2,8 @@
Declaration of variadic function Frama_C_show_each_warning.
[variadic] tests/erroneous/variadic-builtin.i:1:
Variadic builtin Frama_C_show_each_warning left untransformed.
+[variadic] tests/erroneous/variadic-builtin.i:5:
+ Call to variadic builtin Frama_C_show_each_warning left untransformed.
[kernel] tests/erroneous/variadic-builtin.i:6: Plug-in variadic aborted: unimplemented feature.
You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
'[Plug-in variadic] The variadic plugin doesn't handle calls to a pointer to the variadic builtin Frama_C_show_each_warning.'.
diff --git a/src/plugins/variadic/translate.ml b/src/plugins/variadic/translate.ml
index bf32abcdf50d6cae2a3d62bd75df158e77d48e43..04887ec9f26596fd79d24cba26791327ff487e03 100644
--- a/src/plugins/variadic/translate.ml
+++ b/src/plugins/variadic/translate.ml
@@ -27,17 +27,7 @@ module Typ = Extends.Typ
(* List of builtin function names to translate *)
-let va_builtins = [
- "__builtin_va_start";
- "__builtin_va_copy";
- "__builtin_va_arg";
- "__builtin_va_end"]
-
-let is_framac_builtin vi =
- Ast_info.is_frama_c_builtin vi.vname ||
- Cil_builtins.Builtin_functions.mem vi.vname ||
- Extlib.string_prefix "__FRAMAC_" vi.vname (* Mthread prefixes *)
-
+let is_framac_builtin vi = Classify.is_frama_c_builtin vi.vname
(* In place visitor for translation *)
@@ -89,13 +79,14 @@ let translate_variadics (file : file) =
begin match glob with
| GFunDecl(_, vi, _) ->
(match Table.find_opt classification vi with
- | None -> ()
+ | None -> Cil.DoChildren (* may transform the type *)
| Some { vf_class = Builtin } ->
Self.result ~level:2 ~current:true
"Variadic builtin %s left untransformed." vi.vname;
+ Cil.SkipChildren
| Some _ ->
- Generic.add_vpar vi);
- Cil.DoChildren
+ Generic.add_vpar vi;
+ Cil.DoChildren)
| GFun ({svar = vi} as fundec, _) ->
if Table.mem classification vi then begin
@@ -147,7 +138,10 @@ let translate_variadics (file : file) =
| Overload o -> Standard.overloaded_call ~fundec o
| Aggregator a -> Standard.aggregator_call ~fundec ~ghost a
| FormatFun f -> Standard.format_fun_call ~fundec env f
- | Builtin -> raise Not_found
+ | Builtin ->
+ Self.result ~level:2 ~current:true
+ "Call to variadic builtin %s left untransformed." f.vname;
+ raise Not_found
| _ -> raise Standard.Translate_call_exn
in
call_translator block loc mk_call vf args
@@ -157,7 +151,7 @@ let translate_variadics (file : file) =
in
begin match i with
| Call(_, {enode = Lval(Var vi, _)}, _, _)
- when List.mem vi.vname va_builtins ->
+ when Classify.is_va_builtin vi.vname ->
File.must_recompute_cfg fundec;
Cil.ChangeTo (Generic.translate_va_builtin fundec i)
| Call(lv, {enode = Lval(Var vi, NoOffset)}, args, loc) ->