[Builtin] Small fix + Doc

src/plugins/builtin/README.md

+# Builtin plugin
+
+## Description
+
+The builtin plugin is meant to build function specialization to C functions in
+a project when the original specification (or prototype of the function) cannot
+be efficiently used by some plugins.
+
+For example, the specification of a function like `memcpy` cannot be efficiently
+used by a plugin like `WP` because it involves `void*` pointers and requires to
+deduce that bytes equality implies (typed) data equality. While for example it
+is easy to produce a typed specification for a type `int`:
+
+```c
+/*@ requires valid_dest: \valid(dest + (0 .. len-1));
+    requires valid_read_src: \valid_read(src + (0 .. len-1));
+    requires separation: \separated(dest + (0 .. len-1), src + (0 .. len-1));
+    ensures copied: ∀ ℤ j0; 0 ≤ j0 < len ⇒ *(dest + j0) ≡ *(src + j0);
+    ensures result: \result ≡ dest;
+    assigns *(dest + (0 .. len - 1)), \result;
+    assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
+    assigns \result \from dest;
+ */
+int *memcpy_int(int *dest, int const *src, size_t len);
+```
+
+That can be easily used by WP.
+
+The role of the Builtin plugin is to find each call for which a builtin
+generator is available and if the call is well-typed according to the generator
+(for example for `memcpy` if `dest` and `src` are both pointers to integers), to
+replace this call with a call to an automatically generated specialization
+corresponding to the call.
+
+## Options
+
+- `-builtin` activate builtin replacement
+- `-builtin-fct=f,...` only replace calls in specified functions (default to all)
+- `-builtin-(no-)<function_name>` activate or deactivate a particular builtin
+  function, defaults to true.
+
+## Available builtin functions
+
+### `string.h`
+
+```c
+int memcmp(void const* s1, void const* s2, size_t len);
+```
+
+The parameters `s1` and `s2` must have the same types, except that qualifiers
+and typedefs are ignored. The type of `s1` or `s2` cannot be `void*`.
+
+```c
+void* memcpy(void * dest, void const* src, size_t len);
+```
+
+The parameters `dest` and `src` must have the same types, except that qualifiers
+and typedefs are ignored. The type of `dest` or `src` cannot be `void*`.
+
+```c
+void* memmove(void * dest, void const* src, size_t len);
+```
+
+The parameters `dest` and `src` must have the same types, except that qualifiers
+and typedefs are ignored. The type of `dest` or `src` cannot be `void*`.
+
+```c
+void* memset(void * ptr, int value, size_t len);
+```
+
+If `ptr` is of `char*` type (include signed and unsigned variants), `value` must
+be a `char`.
+
+If `ptr` is of any other pointer type (except `void*`), `value` must be a
+constant that statically evaluates to `0x00` or `0xFF`.
+
+### `stdlib.h`
+
+```c
+void* calloc(size_t num, size_t size);
+
+{
+  type* res = calloc(...) ;
+}
+```
+
+`calloc` is typed according to the variable that receives its result. It must be
+a pointer type different from `void*`. If the pointed type has a flexible array
+member, `num` is assumed to evaluate to `1` (a precondition is created for this).
+
+```c
+void free(void* ptr);
+```
+
+The type of `ptr` must be different from `void*`.
+
+
+```c
+void* malloc(size_t num, size_t size);
+
+{
+  type* res = calloc(...) ;
+}
+```
+
+`malloc` is typed according to the variable that receives its result. It must be
+a pointer type different from `void*`.
+
+## Adding a new builtin
+
+To add a new builtin, one has to register a new module implementing the
+`Builtin_builder.Generator_sig` module type to the `Transform` module. The
+lasts steps of the code should look like:
+
+```ocaml
+let () = Transform.register (module struct
+    module Hashtbl = ...
+    type override_key = ...
+
+    let function_name = "my_builtin_function"
+    let well_typed_call = ...
+    let key_from_call = ...
+    let retype_args = ...
+    let generate_prototype = ...
+    let generate_spec = ...
+    let args_for_original = ...
+  end)
+```
+
+The role and types of each function is documented in `Builtin_builder.mli`.
\ No newline at end of file

src/plugins/builtin/basic_blocks.ml

@@ -51,6 +51,7 @@ let call_function lval vi args =
   Call(lval, (Cil.evar vi), args, loc)
 
 let rec string_of_typ_aux = function
+  | TVoid(_) -> "void"
   | TInt(IBool, _) -> "bool"
   | TInt(IChar, _) -> "char"
   | TInt(ISChar, _) -> "schar"
@@ -67,8 +68,9 @@ let rec string_of_typ_aux = function
   | TFloat(FDouble, _) -> "double"
   | TFloat(FLongDouble, _) -> "ldouble"
   | TPtr(t, _) -> "ptr_" ^ string_of_typ t
-  | TEnum (ei, _) -> ei.ename
-  | TComp (ci, _, _) -> ci.cname
+  | TEnum (ei, _) -> "e_" ^ ei.ename
+  | TComp (ci, _, _) when ci.cstruct -> "st_" ^ ci.cname
+  | TComp (ci, _, _) -> "un_" ^ ci.cname
   | TArray (t, Some e, _, _) ->
     "arr" ^ (string_of_exp e) ^ "_" ^ string_of_typ t
   | _ -> assert false

src/plugins/builtin/basic_blocks.mli

@@ -22,44 +22,177 @@
 
 open Cil_types
 
+(** [string_of_typ t] returns a name generated from the given [t]. This is
+    basically the C name of the type except that:
+    - separator is ["_"],
+    - [unsigned] is ["u"]
+    - [[SIZE]] is ["arrSIZE"],
+    - [*] is ["ptr"],
+    - [enum] is ["e_"],
+    - [struct] is ["st_"],
+    - [union] is ["un_"]
+
+    For example for: [struct X ( * ) [10]], the name is ["ptr_arr10_st_X"].
+*)
+val string_of_typ: typ -> string
+
+(** Returns the type of pointed for a give logic_type *)
+val ttype_of_pointed: logic_type -> logic_type
+
+
+(** {2 C} *)
+
+(** For a type [T], returns [T*] *)
 val ptr_of: typ -> typ
+
+(** For a type [T], returns [T const] *)
 val const_of: typ -> typ
 
+(** Finds and returns [size_t] *)
 val size_t: unit -> typ
 
+(** Create a function definition from a name and a type
+    - [vdefined] is positionned to [true]
+    - formals are registered to FormalsDecl
+*)
 val prepare_definition: string -> typ -> fundec
+
+(** [call_function ret_lval vi args] creates an instruction
+    - [(ret_lval = ) vi.vname(args)].
+*)
 val call_function: lval option -> varinfo -> exp list -> instr
 
-val string_of_typ: typ -> string
 
-val ttype_of_pointed: logic_type -> logic_type
+(** {2 Terms} *)
 
+(** Builds a term from a varinfo *)
 val cvar_to_tvar: varinfo -> term
+
+(** [tunref_range ~loc ptr len] builds [*(ptr + (0 .. len-1))] *)
 val tunref_range: ?loc:location -> term -> term -> term
+
+(** [tplus ~loc t1 t2] builds [t1+t2] *)
 val tplus: ?loc:location -> term -> term -> term
+
+(** [tminus ~loc t1 t2] builds [t1-t2] *)
 val tminus: ?loc:location -> term -> term -> term
+
+(** [tdivide ~loc t1 t2] builds [t1/t2] *)
 val tdivide: ?loc:location -> term -> term -> term
 
+
+(** {2 Predicates} *)
+
+(** [pbounds_incl_excl ~loc low v up] builds [low <= v < up]. *)
 val pbounds_incl_excl: ?loc:location -> term -> term -> term -> predicate
-val pvalid_len_bytes: ?loc:location -> logic_label -> term -> term -> predicate
-val pvalid_read_len_bytes:
-  ?loc:location -> logic_label -> term -> term -> predicate
-val pcorrect_len_bytes: ?loc:location -> logic_type -> term -> predicate
+
+(** [plet_len_div_size ~loc ~name_ext ltyp bytes_len pred] buils a predicate:
+    - [\let name = bytes_len / sizeof(ltyp) ; < pred name >]
+
+    with [name = "__fc_<name_ext>len"]. For example, if [pred len] generates an
+    ACSL predicate:
+    - [\forall int x ; 0 <= x < len ==> p[x] == 0],
+
+    [ltyp] is [int], and [bytes_len] is 16, it generates:
+    - [\let __fc_len = bytes_len / sizeof(ltyp) ;
+       \forall int x ; 0 <= x < __fc_len ==> p[x] == 0].
+
+    Parameters:
+    - [loc] defaults to [Cil_datatype.Location.unknown]
+    - [name_ext] defaults to [""]
+    - [ltyp] must be a logic C type
+    - [bytes_len] is a value in bytes that should be divided by the [sizeof(ltyp)]
+    - if the elements contains structures they cannot have flexible array member
+*)
+val plet_len_div_size:
+  ?loc:location -> ?name_ext:string ->
+  logic_type -> term -> (term -> predicate) -> predicate
+
+(** [punfold_all_elems_eq ~loc p1 p2 len] builds a predicate:
+    - [\forall integer j1 ; 0 <= j1 < len ==> p1[j1] == p2[j1]].
+
+    If [p1[j1]] is itself an array, it recursively builds a predicate:
+    - [\forall integer j2 ; 0 <= j2 < len_of_array ==> ...].
+
+    Parameters:
+    - [p1] and [p2] must be pointers to the same type
+*)
 val punfold_all_elems_eq: ?loc:location -> term -> term -> term -> predicate
+
+(** [punfold_all_elems_pred ~loc ptr len pred] builds a predicate:
+    - [\forall integer j ; 0 <= j1 < len ==> < pred (\*(ptr + j1)) >].
+
+    If [ptr[j1]] is a compound type (array or structure), it recursively builds
+    a predicate on each element (either by introducing a new [\forall] for
+    arrays or a conjunction for structure fields).
+
+    - [ptr] must be a pointer
+    - [pred] must be applicable on simple types or pointers
+    - if the elements contains structures they cannot have flexible array member
+*)
 val punfold_all_elems_pred:
   ?loc:location -> term -> term ->
   (?loc: location -> term -> predicate) -> predicate
+
+(** [punfold_flexible_struct_pred ~loc struct bytes_len pred].
+
+    For a [struct] term of C type [struct X { ... ; Type a[]; };], it generates
+    a predicate:
+    - [\let __fc_len = (bytes_len - sizeof(struct X)) / sizeof(Type) ;
+        < pred on struct fields > &&
+        \forall integer j ; 0 <= j <= __fc_len ==> < pred on struct.a[j] >]
+
+    If met components are compound, it behaves like [punfold_all_elems_pred].
+
+    Parameters:
+    - [struct] must be a (term) structure with a flexible array member
+    - [bytes_len] is the length of the structure in bytes
+    - [pred] must be applicable on simple types or pointers
+*)
 val punfold_flexible_struct_pred:
   ?loc:location -> term -> term ->
   (?loc: location -> term -> predicate) -> predicate
 
+(** [pvalid_len_bytes ~loc label ptr bytes_len] generates a predicate
+    - [\valid{label}(ptr + (0 .. (len_bytes/sizeof(\*ptr))))].
+
+    Parameters:
+    - [ptr] must be a term of pointer type.
+*)
+val pvalid_len_bytes: ?loc:location -> logic_label -> term -> term -> predicate
+
+(** [pvalid_read_len_bytes ~loc label ptr bytes_len] generates a predicate
+  - [\valid_read{label}(ptr + (0 .. (len_bytes/sizeof(\*ptr))))].
+
+  Parameters:
+  - [ptr] must be a term of pointer type.
+ *)
+val pvalid_read_len_bytes:
+  ?loc:location -> logic_label -> term -> term -> predicate
+
+(** [pcorrect_len_bytes ~loc ltyp bytes_len] returns a predicate
+    [bytes_len % sizeof(ltyp) == 0].
+*)
+val pcorrect_len_bytes: ?loc:location -> logic_type -> term -> predicate
+
+(** [pseparated_memories ~loc p1 len1 p2 len2] returns a predicate:
+    - [\separated(p1 + (0 .. len1), p2 + (0 .. len2))]
+
+    Parameters:
+    - [p1] and [p2] must be of pointer type
+*)
 val pseparated_memories:
   ?loc:location -> term -> term -> term -> term -> predicate
 
-val plet_len_div_size:
-  ?loc:location -> ?name_ext:string ->
-  logic_type -> term -> (term -> predicate) -> predicate
+(** {2 Specification} *)
 
+(** Builds a behavior from its components. If a component is missing,
+  it defaults to:
+  - [name]: [Cil.default_behavior_name]
+  - [requires], [ensures], [extension]: [[]]
+  - [assigns]: = [WritesAny]
+  - [alloc]: [FreeAllocAny]
+*)
 val make_behavior:
   ?name:string ->
   ?assumes:identified_predicate list ->
@@ -71,6 +204,10 @@ val make_behavior:
   unit ->
   behavior
 
+(** Builds a funspec from a list of behaviors.
+    - [termination] defaults to [None]
+    - [complete_disjoint] default to all disjoint, all complete
+*)
 val make_funspec:
   behavior list ->
   ?termination:identified_predicate option ->

src/plugins/builtin/options.mli

@@ -22,9 +22,16 @@
 
 include Plugin.General_services
 
+(** Builtin transformtion enabled *)
 module Enabled : Parameter_sig.Bool
+
+(** Set of kernel function provided for transformation *)
 module Kfs : Parameter_sig.Kernel_function_set
 
+(** Used by [Builtin_builder] to generate builtin options. For a given builtin,
+    the module generate an option "-builtin-(no-)<function_name>" that defaults
+    to true.
+*)
 module NewBuiltin
     (B : sig val function_name: string end) : Parameter_sig.Bool
 

src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle

@@ -49,7 +49,7 @@ struct Flex {
     complete behaviors no_allocation, allocation;
     disjoint behaviors no_allocation, allocation;
  */
-struct Flex *calloc_Flex(size_t num, size_t size)
+struct Flex *calloc_st_Flex(size_t num, size_t size)
 {
   struct Flex *__retres;
   __retres = (struct Flex *)calloc(num,size);
@@ -170,7 +170,7 @@ char *calloc_char(size_t num, size_t size)
     complete behaviors no_allocation, allocation;
     disjoint behaviors no_allocation, allocation;
  */
-struct X *calloc_X(size_t num, size_t size)
+struct X *calloc_st_X(size_t num, size_t size)
 {
   struct X *__retres;
   __retres = (struct X *)calloc(num,size);
@@ -256,12 +256,12 @@ int main(void)
   int __retres;
   int *pi = calloc_int((unsigned int)10,sizeof(int));
   float *pf = calloc_float((unsigned int)10,sizeof(float));
-  struct X *px = calloc_X((unsigned int)10,sizeof(struct X));
+  struct X *px = calloc_st_X((unsigned int)10,sizeof(struct X));
   char *pc = calloc_char((unsigned int)10,sizeof(char));
   int (*pa)[10] = calloc_arr10_int((unsigned int)10,sizeof(int [10]));
   struct Flex *f =
-    calloc_Flex((unsigned int)1,
-                sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+    calloc_st_Flex((unsigned int)1,
+                   sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
   void *v = calloc((unsigned int)10,sizeof(char));
   __retres = 0;
   return __retres;
@@ -320,7 +320,7 @@ struct Flex {
     complete behaviors no_allocation, allocation;
     disjoint behaviors no_allocation, allocation;
  */
-struct Flex *calloc_Flex(size_t num, size_t size)
+struct Flex *calloc_st_Flex(size_t num, size_t size)
 {
   struct Flex *__retres;
   __retres = (struct Flex *)calloc(num,size);
@@ -444,7 +444,7 @@ char *calloc_char(size_t num, size_t size)
     complete behaviors no_allocation, allocation;
     disjoint behaviors no_allocation, allocation;
  */
-struct X *calloc_X(size_t num, size_t size)
+struct X *calloc_st_X(size_t num, size_t size)
 {
   struct X *__retres;
   __retres = (struct X *)calloc(num,size);
@@ -532,12 +532,12 @@ int main(void)
   int __retres;
   int *pi = calloc_int((unsigned int)10,sizeof(int));
   float *pf = calloc_float((unsigned int)10,sizeof(float));
-  struct X *px = calloc_X((unsigned int)10,sizeof(struct X));
+  struct X *px = calloc_st_X((unsigned int)10,sizeof(struct X));
   char *pc = calloc_char((unsigned int)10,sizeof(char));
   int (*pa)[10] = calloc_arr10_int((unsigned int)10,sizeof(int [10]));
   struct Flex *f =
-    calloc_Flex((unsigned int)1,
-                sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+    calloc_st_Flex((unsigned int)1,
+                   sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
   void *v = calloc((unsigned int)10,sizeof(char));
   __retres = 0;
   return __retres;

src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle

@@ -35,7 +35,7 @@ struct Flex {
     complete behaviors no_allocation, allocation;
     disjoint behaviors no_allocation, allocation;
  */
-struct Flex *malloc_Flex(size_t size)
+struct Flex *malloc_st_Flex(size_t size)
 {
   struct Flex *__retres;
   __retres = (struct Flex *)malloc(size);
@@ -128,7 +128,7 @@ char *malloc_char(size_t size)
     complete behaviors no_allocation, allocation;
     disjoint behaviors no_allocation, allocation;
  */
-struct X *malloc_X(size_t size)
+struct X *malloc_st_X(size_t size)
 {
   struct X *__retres;
   __retres = (struct X *)malloc(size);
@@ -202,11 +202,11 @@ int main(void)
   int __retres;
   int *pi = malloc_int(sizeof(int) * (unsigned int)10);
   float *pf = malloc_float(sizeof(float) * (unsigned int)10);
-  struct X *px = malloc_X(sizeof(struct X) * (unsigned int)10);
+  struct X *px = malloc_st_X(sizeof(struct X) * (unsigned int)10);
   char *pc = malloc_char((unsigned int)10);
   int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10);
   struct Flex *f =
-    malloc_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+    malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
   void *v = malloc(sizeof(char) * (unsigned int)10);
   __retres = 0;
   return __retres;
@@ -252,7 +252,7 @@ struct Flex {
     complete behaviors no_allocation, allocation;
     disjoint behaviors no_allocation, allocation;
  */
-struct Flex *malloc_Flex(size_t size)
+struct Flex *malloc_st_Flex(size_t size)
 {
   struct Flex *__retres;
   __retres = (struct Flex *)malloc(size);
@@ -345,7 +345,7 @@ char *malloc_char(size_t size)
     complete behaviors no_allocation, allocation;
     disjoint behaviors no_allocation, allocation;
  */
-struct X *malloc_X(size_t size)
+struct X *malloc_st_X(size_t size)
 {
   struct X *__retres;
   __retres = (struct X *)malloc(size);
@@ -419,11 +419,11 @@ int main(void)
   int __retres;
   int *pi = malloc_int(sizeof(int) * (unsigned int)10);
   float *pf = malloc_float(sizeof(float) * (unsigned int)10);
-  struct X *px = malloc_X(sizeof(struct X) * (unsigned int)10);
+  struct X *px = malloc_st_X(sizeof(struct X) * (unsigned int)10);
   char *pc = malloc_char((unsigned int)10);
   int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10);
   struct Flex *f =
-    malloc_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+    malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
   void *v = malloc(sizeof(char) * (unsigned int)10);
   __retres = 0;
   return __retres;

src/plugins/builtin/tests/string/oracle/memcmp.res.oracle

@@ -64,7 +64,7 @@ int with_named(named * /*[10]*/ s1, named * /*[10]*/ s2)
       \from (indirect: *(s1 + (0 .. len - 1))),
             (indirect: *(s2 + (0 .. len - 1)));
  */
-int memcmp_X(struct X const *s1, struct X const *s2, size_t len)
+int memcmp_st_X(struct X const *s1, struct X const *s2, size_t len)
 {
   int __retres;
   __retres = memcmp((void const *)s1,(void const *)s2,len);
@@ -74,7 +74,7 @@ int memcmp_X(struct X const *s1, struct X const *s2, size_t len)
 int structure(struct X * /*[10]*/ s1, struct X * /*[10]*/ s2)
 {
   int tmp;
-  tmp = memcmp_X(s1,s2,(unsigned int)10 * sizeof(struct X));
+  tmp = memcmp_st_X(s1,s2,(unsigned int)10 * sizeof(struct X));
   return tmp;
 }
 
@@ -233,7 +233,7 @@ int with_named(named *s1, named *s2)
       \from (indirect: *(s1 + (0 .. len - 1))),
             (indirect: *(s2 + (0 .. len - 1)));
  */
-int memcmp_X(struct X const *s1, struct X const *s2, size_t len)
+int memcmp_st_X(struct X const *s1, struct X const *s2, size_t len)
 {
   int __retres;
   __retres = memcmp((void const *)s1,(void const *)s2,len);
@@ -243,8 +243,8 @@ int memcmp_X(struct X const *s1, struct X const *s2, size_t len)
 int structure(struct X *s1, struct X *s2)
 {
   int tmp;
-  tmp = memcmp_X((struct X const *)s1,(struct X const *)s2,
-                 (unsigned int)10 * sizeof(struct X));
+  tmp = memcmp_st_X((struct X const *)s1,(struct X const *)s2,
+                    (unsigned int)10 * sizeof(struct X));
   return tmp;
 }
 

src/plugins/builtin/tests/string/oracle/memcpy.res.oracle

@@ -69,7 +69,7 @@ void with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
     assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
     assigns \result \from dest;
  */
-struct X *memcpy_X(struct X *dest, struct X const *src, size_t len)
+struct X *memcpy_st_X(struct X *dest, struct X const *src, size_t len)
 {
   struct X *__retres;
   __retres = (struct X *)memcpy((void *)dest,(void const *)src,len);
@@ -78,8 +78,8 @@ struct X *memcpy_X(struct X *dest, struct X const *src, size_t len)
 
 void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
 {
-  struct X *res = memcpy_X(dest,src,(unsigned int)10 * sizeof(struct X));
-  memcpy_X(src,res,(unsigned int)10 * sizeof(struct X));
+  struct X *res = memcpy_st_X(dest,src,(unsigned int)10 * sizeof(struct X));
+  memcpy_st_X(src,res,(unsigned int)10 * sizeof(struct X));
   return;
 }
 
@@ -249,7 +249,7 @@ void with_named(named *src, named *dest)
     assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
     assigns \result \from dest;
  */
-struct X *memcpy_X(struct X *dest, struct X const *src, size_t len)
+struct X *memcpy_st_X(struct X *dest, struct X const *src, size_t len)
 {
   struct X *__retres;
   __retres = (struct X *)memcpy((void *)dest,(void const *)src,len);
@@ -259,8 +259,9 @@ struct X *memcpy_X(struct X *dest, struct X const *src, size_t len)
 void structure(struct X *src, struct X *dest)
 {
   struct X *res =
-    memcpy_X(dest,(struct X const *)src,(unsigned int)10 * sizeof(struct X));
-  memcpy_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
+    memcpy_st_X(dest,(struct X const *)src,
+                (unsigned int)10 * sizeof(struct X));
+  memcpy_st_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
   return;
 }
 

src/plugins/builtin/tests/string/oracle/memmove.res.oracle

@@ -61,7 +61,7 @@ void with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
     assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
     assigns \result \from dest;
  */
-struct X *memmove_X(struct X *dest, struct X const *src, size_t len)
+struct X *memmove_st_X(struct X *dest, struct X const *src, size_t len)
 {
   struct X *__retres;
   __retres = (struct X *)memmove((void *)dest,(void const *)src,len);
@@ -70,8 +70,8 @@ struct X *memmove_X(struct X *dest, struct X const *src, size_t len)
 
 void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
 {
-  struct X *res = memmove_X(dest,src,(unsigned int)10 * sizeof(struct X));
-  memmove_X(src,res,(unsigned int)10 * sizeof(struct X));
+  struct X *res = memmove_st_X(dest,src,(unsigned int)10 * sizeof(struct X));
+  memmove_st_X(src,res,(unsigned int)10 * sizeof(struct X));
   return;
 }
 
@@ -225,7 +225,7 @@ void with_named(named *src, named *dest)
     assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
     assigns \result \from dest;
  */
-struct X *memmove_X(struct X *dest, struct X const *src, size_t len)
+struct X *memmove_st_X(struct X *dest, struct X const *src, size_t len)
 {
   struct X *__retres;
   __retres = (struct X *)memmove((void *)dest,(void const *)src,len);
@@ -235,8 +235,9 @@ struct X *memmove_X(struct X *dest, struct X const *src, size_t len)
 void structure(struct X *src, struct X *dest)
 {
   struct X *res =
-    memmove_X(dest,(struct X const *)src,(unsigned int)10 * sizeof(struct X));
-  memmove_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
+    memmove_st_X(dest,(struct X const *)src,
+                 (unsigned int)10 * sizeof(struct X));
+  memmove_st_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
   return;
 }
 

src/plugins/builtin/tests/string/oracle/memset_0.res.oracle

@@ -157,7 +157,7 @@ void with_named(named * /*[10]*/ dest)
     assigns *(ptr + (0 .. num - 1)) \from \nothing;
     assigns \result \from ptr;
  */
-struct X *memset_X_0(struct X *ptr, size_t num)
+struct X *memset_st_X_0(struct X *ptr, size_t num)
 {
   struct X *__retres;
   __retres = (struct X *)memset((void *)ptr,0,num);
@@ -166,8 +166,8 @@ struct X *memset_X_0(struct X *ptr, size_t num)
 
 void structure(struct X * /*[10]*/ dest)
 {
-  struct X *res = memset_X_0(dest,(unsigned int)10 * sizeof(struct X));
-  memset_X_0(res,(unsigned int)10 * sizeof(struct X));
+  struct X *res = memset_st_X_0(dest,(unsigned int)10 * sizeof(struct X));
+  memset_st_X_0(res,(unsigned int)10 * sizeof(struct X));
   return;
 }
 
@@ -418,7 +418,7 @@ void with_named(named *dest)
     assigns *(ptr + (0 .. num - 1)) \from \nothing;
     assigns \result \from ptr;
  */
-struct X *memset_X_0(struct X *ptr, size_t num)
+struct X *memset_st_X_0(struct X *ptr, size_t num)
 {
   struct X *__retres;
   __retres = (struct X *)memset((void *)ptr,0,num);
@@ -427,8 +427,8 @@ struct X *memset_X_0(struct X *ptr, size_t num)
 
 void structure(struct X *dest)
 {
-  struct X *res = memset_X_0(dest,(unsigned int)10 * sizeof(struct X));
-  memset_X_0(res,(unsigned int)10 * sizeof(struct X));
+  struct X *res = memset_st_X_0(dest,(unsigned int)10 * sizeof(struct X));
+  memset_st_X_0(res,(unsigned int)10 * sizeof(struct X));
   return;
 }
 

src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle

@@ -295,7 +295,7 @@ void with_named(named * /*[10]*/ dest)
     assigns *(ptr + (0 .. num - 1)) \from \nothing;
     assigns \result \from ptr;
  */
-struct X *memset_X_FF(struct X *ptr, size_t num)
+struct X *memset_st_X_FF(struct X *ptr, size_t num)
 {
   struct X *__retres;
   __retres = (struct X *)memset((void *)ptr,255,num);
@@ -304,8 +304,8 @@ struct X *memset_X_FF(struct X *ptr, size_t num)
 
 void structure(struct X * /*[10]*/ dest)
 {
-  struct X *res = memset_X_FF(dest,(unsigned int)10 * sizeof(struct X));
-  memset_X_FF(res,(unsigned int)10 * sizeof(struct X));
+  struct X *res = memset_st_X_FF(dest,(unsigned int)10 * sizeof(struct X));
+  memset_st_X_FF(res,(unsigned int)10 * sizeof(struct X));
   return;
 }
 
@@ -704,7 +704,7 @@ void with_named(named *dest)
     assigns *(ptr + (0 .. num - 1)) \from \nothing;
     assigns \result \from ptr;
  */
-struct X *memset_X_FF(struct X *ptr, size_t num)
+struct X *memset_st_X_FF(struct X *ptr, size_t num)
 {
   struct X *__retres;
   __retres = (struct X *)memset((void *)ptr,255,num);
@@ -713,8 +713,8 @@ struct X *memset_X_FF(struct X *ptr, size_t num)
 
 void structure(struct X *dest)
 {
-  struct X *res = memset_X_FF(dest,(unsigned int)10 * sizeof(struct X));
-  memset_X_FF(res,(unsigned int)10 * sizeof(struct X));
+  struct X *res = memset_st_X_FF(dest,(unsigned int)10 * sizeof(struct X));
+  memset_st_X_FF(res,(unsigned int)10 * sizeof(struct X));
   return;
 }
 

src/plugins/builtin/transform.mli

@@ -20,5 +20,17 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** Module for AST transformation *)
+
+(** Registers a new [Builtin] to the visitor from the [Generator_sig] module
+    of this builtin. Each new builtin function generator should call this
+    globally.
+*)
 val register: (module Builtin_builder.Generator_sig) -> unit
+
+(** In all selected functions of the given file, for all function call, if there
+    exists a builtin module for this function, and the call is well-typed,
+    replaces it with a call to the generated override function and inserted the
+    generated function in the AST.
+*)
 val transform: Cil_types.file -> unit