diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml index c8588932c9f16984631e4e585496b84d3849dd12..283c8dd8384edd64e13c4b9282ce5361f03f2c11 100644 --- a/src/plugins/value/domains/cvalue/builtins_malloc.ml +++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml @@ -405,7 +405,7 @@ let alloc_imprecise_weakest_alloc region _stack _prefix _sizev _state = in let var = create_new_var stack "alloc" type_base Weak in Value_parameters.warning ~wkey:wkey_imprecise_alloc ~current:true ~once:true - "@[warning: allocating a single weak variable for ALL dynamic allocations %s: %a@]" + "allocating a single weak variable for ALL dynamic allocations %s: %a" (string_of_region region) Printer.pp_varinfo var; let variable_v = Base.create_variable_validity ~weak:true ~min_alloc:Int.minus_one ~max_alloc:(Bit_utils.max_bit_address ()) in diff --git a/tests/builtins/oracle/calloc.5.res.oracle b/tests/builtins/oracle/calloc.5.res.oracle index 6d2516fe5edda554a96cf8a83f05aa17dd15d16b..31723119f89a996ac6e173c1818e4a29e79773f2 100644 --- a/tests/builtins/oracle/calloc.5.res.oracle +++ b/tests/builtins/oracle/calloc.5.res.oracle @@ -7,7 +7,7 @@ [eva] tests/builtins/calloc.c:14: Call to builtin Frama_C_calloc_imprecise_weakest for function calloc [eva:malloc:imprecise] tests/builtins/calloc.c:14: Warning: - warning: allocating a single weak variable for ALL dynamic allocations via malloc/calloc/realloc: __alloc_w_main + allocating a single weak variable for ALL dynamic allocations via malloc/calloc/realloc: __alloc_w_main [eva] tests/builtins/calloc.c:17: Call to builtin Frama_C_calloc_imprecise_weakest for function calloc [eva] tests/builtins/calloc.c:20: diff --git a/tests/builtins/oracle/malloc.res.oracle b/tests/builtins/oracle/malloc.res.oracle index 558c45624470cb46c1b7aef68a489e060f4257c3..0fd1847bc24a81cb74b70c8b051e0b3bd49c3825 100644 --- a/tests/builtins/oracle/malloc.res.oracle +++ b/tests/builtins/oracle/malloc.res.oracle @@ -37,7 +37,7 @@ [eva] tests/builtins/malloc.c:33: Call to builtin Frama_C_malloc_imprecise_weakest [eva:malloc:imprecise] tests/builtins/malloc.c:33: Warning: - warning: allocating a single weak variable for ALL dynamic allocations via malloc/calloc/realloc: __alloc_w_main + allocating a single weak variable for ALL dynamic allocations via malloc/calloc/realloc: __alloc_w_main [eva] tests/builtins/malloc.c:33: Call to builtin Frama_C_malloc_imprecise_weakest [eva:alarm] tests/builtins/malloc.c:34: Warning: diff --git a/tests/builtins/oracle/realloc_imprecise.res.oracle b/tests/builtins/oracle/realloc_imprecise.res.oracle index 05f617bdea13f3d831a369c411b755c62222fca4..7bb0194ab391b9b43b9f6e1acb0166aac58cfd7a 100644 --- a/tests/builtins/oracle/realloc_imprecise.res.oracle +++ b/tests/builtins/oracle/realloc_imprecise.res.oracle @@ -7,7 +7,7 @@ [eva] tests/builtins/realloc_imprecise.c:10: Call to builtin Frama_C_malloc_imprecise_weakest for function malloc [eva:malloc:imprecise] tests/builtins/realloc_imprecise.c:10: Warning: - warning: allocating a single weak variable for ALL dynamic allocations via malloc/calloc/realloc: __alloc_w_main + allocating a single weak variable for ALL dynamic allocations via malloc/calloc/realloc: __alloc_w_main [eva:alarm] tests/builtins/realloc_imprecise.c:11: Warning: out of bounds write. assert \valid(p); [eva] tests/builtins/realloc_imprecise.c:13: