From fd491709624925948a8356a4cfd207c529270511 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Tue, 14 Feb 2017 17:26:26 +0100
Subject: [PATCH] add locations for warnings
---
src/plugins/e-acsl/mmodel_analysis.ml | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/mmodel_analysis.ml b/src/plugins/e-acsl/mmodel_analysis.ml
index 7d4288f3de6..d0098cee33c 100644
--- a/src/plugins/e-acsl/mmodel_analysis.ml
+++ b/src/plugins/e-acsl/mmodel_analysis.ml
@@ -497,7 +497,7 @@ let register_predicate kf pred state =
params
l
with Invalid_argument _ ->
- Options.warning
+ Options.warning ~current:true
"ignoring effect of variadic function %a"
Kernel_function.pretty
kf;
@@ -522,8 +522,8 @@ let register_predicate kf pred state =
in
Dataflow.Done (Some state)
| _ ->
- Options.warning "function pointers may introduce too limited \
-instrumentation.";
+ Options.warning ~current:true
+ "function pointers may introduce too limited instrumentation.";
(* imprecise function call: keep each argument *)
Dataflow.Done
(Some
--
GitLab