diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml index 2efd15c1339cc2ae87388ec5cebc443cd29f3b8f..2ef662541880c49efc088cbb4bec04dcc90fbe65 100644 --- a/src/plugins/value/domains/cvalue/builtins_malloc.ml +++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml @@ -60,7 +60,7 @@ let () = Ast.add_monotonic_state Dynamic_Alloc_Bases.self let call_stack_no_wrappers () = let stack = Value_util.call_stack () in assert (stack != []); - let wrappers = Value_parameters.MallocFunctions.get() in + let wrappers = Value_parameters.AllocFunctions.get() in let rec bottom_filter = function | [] -> assert false | [_] as stack -> stack (* Do not empty the stack completely *) diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml index a56b71755be5a1106cbe0d50d70965a98076504a..8a3c6adf265da929fab73d7083933b3696d3c5bc 100644 --- a/src/plugins/value/value_parameters.ml +++ b/src/plugins/value/value_parameters.ml @@ -1459,18 +1459,22 @@ let () = add_precision_dep ReductionDepth.parameter (* -------------------------------------------------------------------------- *) let () = Parameter_customize.set_group malloc -module MallocFunctions= +module AllocFunctions = Filled_string_set (struct - let option_name = "-eva-malloc-functions" + let option_name = "-eva-alloc-functions" let arg_name = "f1,...,fn" - let help = "The malloc builtins use the call site of malloc() to know \ + let help = "Controls call site creation for dynamically allocated bases. \ + Dynamic allocation builtins use the call sites of \ + malloc/calloc/realloc to know \ where to create new bases. This detection does not work for \ - custom allocators or wrappers on top of malloc, unless they \ - are listed here. By default, only contains malloc." - let default = Datatype.String.Set.singleton "malloc" + custom allocators or wrappers on top of them, unless they \ + are listed here. \ + By default, contains malloc, calloc and realloc." + let default = Datatype.String.Set.of_list ["malloc"; "calloc"; "realloc"] end) -let () = MallocFunctions.add_aliases ["-val-malloc-functions"] +let () = AllocFunctions.add_aliases ["-val-malloc-functions"] +let () = AllocFunctions.add_aliases ["-eva-malloc-functions"] let () = Parameter_customize.set_group malloc module AllocReturnsNull= diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli index f4a069d86ed4859e3deec979674f55ed24463f52..48882970b088232c190d10c9be7b8cb9b5d9c9d9 100644 --- a/src/plugins/value/value_parameters.mli +++ b/src/plugins/value/value_parameters.mli @@ -162,7 +162,7 @@ module StopAtNthAlarm: Parameter_sig.Int (** Dynamic allocation *) -module MallocFunctions: Parameter_sig.String_set +module AllocFunctions: Parameter_sig.String_set module AllocReturnsNull: Parameter_sig.Bool module MallocLevel: Parameter_sig.Int diff --git a/tests/builtins/malloc-optimistic.c b/tests/builtins/malloc-optimistic.c index 1d1afd57f2a6609edad41df6f60d48e36328525c..d5a922355cef26fc4fd6fd482771381ce6dea6ba 100644 --- a/tests/builtins/malloc-optimistic.c +++ b/tests/builtins/malloc-optimistic.c @@ -1,5 +1,5 @@ /* run.config* - STDOPT: +"-slevel 30 -eva-slevel-merge-after-loop @all -eva-malloc-functions malloc -eva-memexec" + STDOPT: +"-slevel 30 -eva-slevel-merge-after-loop @all -eva-memexec" */ #include <stddef.h> //@ assigns \result \from \nothing; diff --git a/tests/builtins/malloc-size-zero.c b/tests/builtins/malloc-size-zero.c index fdb0c68a7895865ceebc92dfed9ccbd6286aeda6..0ff4c5e749f9ed70eb450993db8dcad2226ca561 100644 --- a/tests/builtins/malloc-size-zero.c +++ b/tests/builtins/malloc-size-zero.c @@ -1,6 +1,6 @@ /* run.config* OPT: -eva @EVA_CONFIG@ -eva-mlevel 3 - OPT: -eva @EVA_CONFIG@ -eva-malloc-functions my_calloc + OPT: -eva @EVA_CONFIG@ -eva-alloc-functions my_calloc */ #include <stdlib.h> diff --git a/tests/builtins/memexec-malloc.c b/tests/builtins/memexec-malloc.c index 13755b28f84a30df2756040668f35c799571097f..39b1658ba7681532d456aecf4e5c0666de79cd65 100644 --- a/tests/builtins/memexec-malloc.c +++ b/tests/builtins/memexec-malloc.c @@ -1,5 +1,5 @@ /* run.config* - STDOPT: #"-eva-malloc-functions alloc -eva-mlevel 0" + STDOPT: #"-eva-alloc-functions alloc -eva-mlevel 0" */ #include <stdlib.h> #define N 2000 diff --git a/tests/builtins/realloc.c b/tests/builtins/realloc.c index 4fa6f7f5b55b6cc8addec0b44a3a0965ebc1bb9b..08db98c71601626d53a0f0f78f31fe799cbff246 100644 --- a/tests/builtins/realloc.c +++ b/tests/builtins/realloc.c @@ -1,5 +1,5 @@ /* run.config* - STDOPT: +"-slevel 10 -eva-builtin malloc:Frama_C_malloc_fresh -eva-malloc-functions malloc,realloc -eva-warn-copy-indeterminate @all" + STDOPT: +"-slevel 10 -eva-builtin malloc:Frama_C_malloc_fresh -eva-warn-copy-indeterminate @all" */ #include <stdlib.h>