From 1ce80086247d41810333b96cb7403cb3fd05416d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 1 Apr 2020 14:41:52 +0200
Subject: [PATCH] [Eva] Fixes a warning warning message.
---
src/plugins/value/domains/cvalue/builtins_malloc.ml | 2 +-
tests/builtins/oracle/calloc.5.res.oracle | 2 +-
tests/builtins/oracle/malloc.res.oracle | 2 +-
tests/builtins/oracle/realloc_imprecise.res.oracle | 2 +-
4 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index c8588932c9f..283c8dd8384 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 6d2516fe5ed..31723119f89 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 558c4562447..0fd1847bc24 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 05f617bdea1..7bb0194ab39 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:
--
GitLab