diff --git a/src/plugins/e-acsl/functions.ml b/src/plugins/e-acsl/functions.ml
index d50c077ad8f3be384c85f914230f8e35076ab4f3..189208b355b0e7c3a1f4e39f1bea6bfb9d3b27c1 100644
--- a/src/plugins/e-acsl/functions.ml
+++ b/src/plugins/e-acsl/functions.ml
@@ -70,6 +70,8 @@ module RTL: sig
val is_generated_literal_string_name: string -> bool
val is_generated_kf: kernel_function -> bool
val get_original_name: kernel_function -> string
+ val get_rtl_replacement_name: string -> string
+ val has_rtl_replacement: string -> bool
end = struct
(* prefix of all functions/variables from the public E-ACSL API *)
@@ -78,6 +80,10 @@ end = struct
(* prefix of temporal analysis functions of the public E-ACSL API *)
let e_acsl_temporal_prefix = e_acsl_api_prefix ^ "temporal_"
+ (* prefix of all builtin functions/variables from the public E-ACSL API,
+ Builtin functions replace original calls in programs. *)
+ let e_acsl_builtin_prefix = e_acsl_api_prefix ^ "builtin_"
+
(* prefix of functions/variables generated by E-ACSL *)
let e_acsl_gen_prefix = "__gen_e_acsl_"
@@ -102,6 +108,13 @@ end = struct
let is_generated_literal_string_name name =
startswith e_acsl_lit_string_prefix name
+
+ let get_rtl_replacement_name fn = e_acsl_builtin_prefix ^ fn
+
+ let has_rtl_replacement = function
+ | "strcpy" | "strncpy" | "strlen" | "strcat" | "strncat" | "strcmp"
+ | "strncmp" | "memcpy" | "memset" | "memcmp" | "memmove" -> true
+ | _ -> false
end
(* }}} *)
@@ -124,6 +137,10 @@ module Libc: sig
val is_vla_alloc_name: string -> bool
val is_alloca: exp -> bool
val is_alloca_name: string -> bool
+ val is_printf: exp -> bool
+ val is_printf_name: string -> bool
+ val printf_fmt_position: string -> int
+ val get_printf_argument_str: loc:location -> string -> exp list -> exp
val actual_alloca: string
end = struct
let is_dyn_alloc_name name =
@@ -156,5 +173,72 @@ end = struct
let is_memcpy exp = is_fn is_memcpy_name exp
let is_memset exp = is_fn is_memset_name exp
+
+ let printf_fmt_position = function
+ | "printf" -> 1
+ | "syslog" | "dprintf" | "fprintf" | "sprintf" -> 2
+ | "snprintf" -> 3
+ | _ -> 0
+
+ let is_printf_name name = printf_fmt_position name <> 0
+
+ let is_printf exp = is_fn is_printf_name exp
+
+ let get_printf_argument_str ~loc fn args =
+ assert (is_printf_name fn);
+ (* drop first n elements from a list *)
+ let rec drop n l =
+ assert (n >= 0);
+ if n > 0 then drop (n-1) (match l with _::e -> e | [] -> [])
+ else l
+ in
+ (* get a character representing an integer type *)
+ let get_ikind_str = function
+ | IInt -> "d" (* [int] *)
+ | IUInt -> "D" (* [unsigned int] *)
+ | ILong -> "l" (* [long] *)
+ | IULong -> "L" (* [unsigned long] *)
+ | ILongLong -> "r" (* [long long] *)
+ | IULongLong -> "R" (* [unsigned long long] *)
+ (* _Bool, char and short (either signed or unsigned are promoted to int) *)
+ | IBool | IChar | ISChar | IUChar | IShort | IUShort -> "d"
+ in
+ (* get a character representing an floating point type *)
+ let get_fkind_str = function
+ (* Format-based functions expect only double-precision floats.
+ Single-precision floating points are promoted to doubles so
+ this case should never happen in fact. *)
+ | FFloat -> "f" (* [float] *)
+ | FDouble -> "e" (* [float/double] *)
+ | FLongDouble -> "E" (* [long double] *)
+ in
+ (* get a character representing a pointer type *)
+ let get_pkind_str ty = match ty with
+ | TInt(IChar,_) | TInt(ISChar,_) -> "s" (* [char*] *)
+ | TInt(IUChar,_) -> "S" (* [unsigned char*] *)
+ | TInt(IShort,_) -> "q" (* [short*] *)
+ | TInt(IUShort,_) -> "Q" (* [unsigned short*] *)
+ | TInt(IInt,_) -> "i" (* [int*] *)
+ | TInt(IUInt,_) -> "I" (* [unsigned int*] *)
+ | TInt(ILong,_) -> "z" (* [long int*] *)
+ | TInt(IULong,_) -> "Z" (* [unsigned long int*] *)
+ | TInt(ILongLong,_) -> "w" (* [long int*] *)
+ | TInt(IULongLong,_) -> "W" (* [unsigned long int*] *)
+ | TVoid _ -> "p" (* [void*] *)
+ | _ -> Options.fatal "Unexpected argument type in printf: %a @."
+ Printer.pp_typ ty
+ in
+ let exps = drop (printf_fmt_position fn) args in
+ let param_str = List.fold_left
+ (fun acc exp ->
+ match Cil.unrollTypeDeep (Cil.typeOf exp) with
+ | TInt(k,_) -> acc ^ get_ikind_str k
+ | TFloat(k,_) -> acc ^ get_fkind_str k
+ | TPtr(ty,_) -> acc ^ get_pkind_str ty
+ | TVoid _ | TArray _ | TFun _ | TNamed _ | TComp _ | TEnum _
+ | TBuiltin_va_list _ -> assert false)
+ ""
+ exps
+ in Cil.mkString ~loc param_str
end
(* }}} *)
diff --git a/src/plugins/e-acsl/functions.mli b/src/plugins/e-acsl/functions.mli
index ded776ae5011b7134fe59ce6e91e5646b625f35f..8c1a382e052cfff54637d2f9a91864deae594228 100644
--- a/src/plugins/e-acsl/functions.mli
+++ b/src/plugins/e-acsl/functions.mli
@@ -67,6 +67,14 @@ module RTL: sig
val get_original_name: kernel_function -> string
(** Retrieve the name of the kernel function and strip prefix that indicates
that it has been generated by the instrumentation. *)
+
+ val get_rtl_replacement_name: string -> string
+ (** Given the name of C library function return the name of the RTL function
+ that potentially replaces it. *)
+
+ val has_rtl_replacement: string -> bool
+ (** Given the name of C library function return true if there is a drop-in
+ replacement function for it in the RTL. *)
end
(* ************************************************************************** *)
@@ -124,6 +132,42 @@ module Libc: sig
val is_alloca_name: string -> bool
(** Same as [is_alloca] but for strings *)
+ val is_printf: exp -> bool
+ (** Return [true] if [exp] captures a function name that matches
+ a printf-like function such as [printf], [fprintf], [dprintf] etc. *)
+
+ val is_printf_name: string -> bool
+ (** Same as [is_printf] but for strings *)
+
+ val printf_fmt_position: string -> int
+ (** Given the name of a printf-like function (as determined by
+ [is_printf_name]) return the number of arguments preceding its variadic
+ arguments. *)
+
+ val get_printf_argument_str: loc:location -> string -> exp list -> exp
+ (** Given the name of a printf-like function ([string]) and the list
+ of its variadic arguments [exp list] return a literal string expression
+ where each character describes the type of an argument from a list.
+ Such characters are also called abbreviated types. Conversion between
+ abbreviated and C types characters is as follows:
+ - "b" -> [_Bool]
+ - "c" -> [signed char]
+ - "C" -> [unsigned char]
+ - "d" -> [int]
+ - "D" -> [unsigned int]
+ - "h" -> [short]
+ - "H" -> [unsigned short]
+ - "l" -> [long]
+ - "L" -> [unsigned long]
+ - "r" -> [long long]
+ - "R" -> [unsigned long long]
+ - "f" -> [float]
+ - "e" -> [double]
+ - "E" -> [long double]
+ - "s" -> [char*]
+ - "i" -> [int*]
+ - "p" -> [void*] *)
+
val actual_alloca: string
(** The name of an actual [alloca] function used at link-time.
In GCC/Clang [alloca] is typically implemented via [__builtin_alloca] *)