From daeed27eba8cab04b59b324374dfa0fca08cbd61 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 27 Mar 2020 17:35:38 +0100
Subject: [PATCH] [Instantiate] Changes error when can't instantiate

---
 src/plugins/instantiate/Instantiate.mli       |  2 +-
 src/plugins/instantiate/string/mem_utils.mli  |  2 +-
 .../tests/stdlib/oracle/calloc.res.oracle     |  6 ++--
 .../tests/stdlib/oracle/free.res.oracle       |  3 +-
 .../tests/stdlib/oracle/malloc.res.oracle     |  6 ++--
 .../tests/string/oracle/memcmp.res.oracle     | 18 ++++++----
 .../tests/string/oracle/memcpy.res.oracle     | 24 ++++++++-----
 .../tests/string/oracle/memmove.res.oracle    | 24 ++++++++-----
 .../tests/string/oracle/memset_0.res.oracle   | 12 ++++---
 .../tests/string/oracle/memset_FF.res.oracle  | 12 ++++---
 .../oracle/memset_nested_union.res.oracle     |  2 +-
 .../string/oracle/memset_value.res.oracle     | 36 +++++++++----------
 src/plugins/instantiate/transform.ml          |  3 +-
 13 files changed, 93 insertions(+), 57 deletions(-)

diff --git a/src/plugins/instantiate/Instantiate.mli b/src/plugins/instantiate/Instantiate.mli
index 4af9d03fc53..aaddb8131d0 100644
--- a/src/plugins/instantiate/Instantiate.mli
+++ b/src/plugins/instantiate/Instantiate.mli
@@ -110,4 +110,4 @@ module Global_vars:sig
       transformation.
   *)
   val get: typ -> bool -> storage -> string -> varinfo
-end
\ No newline at end of file
+end
diff --git a/src/plugins/instantiate/string/mem_utils.mli b/src/plugins/instantiate/string/mem_utils.mli
index fca57bd58d0..a6bbb923b7c 100644
--- a/src/plugins/instantiate/string/mem_utils.mli
+++ b/src/plugins/instantiate/string/mem_utils.mli
@@ -72,4 +72,4 @@ type pointed_expr_type =
   | Value_of of typ
   | No_pointed
 
-val exp_type_of_pointed: exp -> pointed_expr_type
\ No newline at end of file
+val exp_type_of_pointed: exp -> pointed_expr_type
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
index cc72848fd62..16706418268 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
@@ -1,6 +1,8 @@
 [kernel] Parsing tests/stdlib/calloc.c (with preprocessing)
-[instantiate] tests/stdlib/calloc.c:24: Warning: Ignore call: not well typed
-[instantiate] tests/stdlib/calloc.c:25: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/calloc.c:24: Warning: 
+  calloc instantiator cannot replace call
+[instantiate] tests/stdlib/calloc.c:25: Warning: 
+  calloc instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stdlib.h"
 struct X {
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
index cfdb769ed8d..a0671fe0bc8 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
@@ -1,5 +1,6 @@
 [kernel] Parsing tests/stdlib/free.c (with preprocessing)
-[instantiate] tests/stdlib/free.c:13: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/free.c:13: Warning: 
+  free instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stdlib.h"
 struct incomplete;
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
index 6cec0abadff..9aff502467c 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
@@ -1,6 +1,8 @@
 [kernel] Parsing tests/stdlib/malloc.c (with preprocessing)
-[instantiate] tests/stdlib/malloc.c:23: Warning: Ignore call: not well typed
-[instantiate] tests/stdlib/malloc.c:24: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/malloc.c:23: Warning: 
+  malloc instantiator cannot replace call
+[instantiate] tests/stdlib/malloc.c:24: Warning: 
+  malloc instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stdlib.h"
 struct X {
diff --git a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
index 856300f9ad0..1f82bcd57b0 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
@@ -1,10 +1,16 @@
 [kernel] Parsing tests/string/memcmp.c (with preprocessing)
-[instantiate] tests/string/memcmp.c:31: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcmp.c:36: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcmp.c:40: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcmp.c:41: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcmp.c:42: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcmp.c:43: Warning: Ignore call: not well typed
+[instantiate] tests/string/memcmp.c:31: Warning: 
+  memcmp instantiator cannot replace call
+[instantiate] tests/string/memcmp.c:36: Warning: 
+  memcmp instantiator cannot replace call
+[instantiate] tests/string/memcmp.c:40: Warning: 
+  memcmp instantiator cannot replace call
+[instantiate] tests/string/memcmp.c:41: Warning: 
+  memcmp instantiator cannot replace call
+[instantiate] tests/string/memcmp.c:42: Warning: 
+  memcmp instantiator cannot replace call
+[instantiate] tests/string/memcmp.c:43: Warning: 
+  memcmp instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
diff --git a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
index 35a4b88ca8f..899dd8afefc 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
@@ -1,12 +1,20 @@
 [kernel] Parsing tests/string/memcpy.c (with preprocessing)
-[instantiate] tests/string/memcpy.c:36: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcpy.c:37: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcpy.c:42: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcpy.c:43: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcpy.c:47: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcpy.c:48: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcpy.c:49: Warning: Ignore call: not well typed
-[instantiate] tests/string/memcpy.c:50: Warning: Ignore call: not well typed
+[instantiate] tests/string/memcpy.c:36: Warning: 
+  memcpy instantiator cannot replace call
+[instantiate] tests/string/memcpy.c:37: Warning: 
+  memcpy instantiator cannot replace call
+[instantiate] tests/string/memcpy.c:42: Warning: 
+  memcpy instantiator cannot replace call
+[instantiate] tests/string/memcpy.c:43: Warning: 
+  memcpy instantiator cannot replace call
+[instantiate] tests/string/memcpy.c:47: Warning: 
+  memcpy instantiator cannot replace call
+[instantiate] tests/string/memcpy.c:48: Warning: 
+  memcpy instantiator cannot replace call
+[instantiate] tests/string/memcpy.c:49: Warning: 
+  memcpy instantiator cannot replace call
+[instantiate] tests/string/memcpy.c:50: Warning: 
+  memcpy instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
diff --git a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
index b53227bdabf..f327581499b 100644
--- a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
@@ -1,12 +1,20 @@
 [kernel] Parsing tests/string/memmove.c (with preprocessing)
-[instantiate] tests/string/memmove.c:36: Warning: Ignore call: not well typed
-[instantiate] tests/string/memmove.c:37: Warning: Ignore call: not well typed
-[instantiate] tests/string/memmove.c:42: Warning: Ignore call: not well typed
-[instantiate] tests/string/memmove.c:43: Warning: Ignore call: not well typed
-[instantiate] tests/string/memmove.c:47: Warning: Ignore call: not well typed
-[instantiate] tests/string/memmove.c:48: Warning: Ignore call: not well typed
-[instantiate] tests/string/memmove.c:49: Warning: Ignore call: not well typed
-[instantiate] tests/string/memmove.c:50: Warning: Ignore call: not well typed
+[instantiate] tests/string/memmove.c:36: Warning: 
+  memmove instantiator cannot replace call
+[instantiate] tests/string/memmove.c:37: Warning: 
+  memmove instantiator cannot replace call
+[instantiate] tests/string/memmove.c:42: Warning: 
+  memmove instantiator cannot replace call
+[instantiate] tests/string/memmove.c:43: Warning: 
+  memmove instantiator cannot replace call
+[instantiate] tests/string/memmove.c:47: Warning: 
+  memmove instantiator cannot replace call
+[instantiate] tests/string/memmove.c:48: Warning: 
+  memmove instantiator cannot replace call
+[instantiate] tests/string/memmove.c:49: Warning: 
+  memmove instantiator cannot replace call
+[instantiate] tests/string/memmove.c:50: Warning: 
+  memmove instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
index af6a60f7c80..dae2db7eba3 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
@@ -1,8 +1,12 @@
 [kernel] Parsing tests/string/memset_0.c (with preprocessing)
-[instantiate] tests/string/memset_0.c:62: Warning: Ignore call: not well typed
-[instantiate] tests/string/memset_0.c:63: Warning: Ignore call: not well typed
-[instantiate] tests/string/memset_0.c:67: Warning: Ignore call: not well typed
-[instantiate] tests/string/memset_0.c:68: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_0.c:62: Warning: 
+  memset instantiator cannot replace call
+[instantiate] tests/string/memset_0.c:63: Warning: 
+  memset instantiator cannot replace call
+[instantiate] tests/string/memset_0.c:67: Warning: 
+  memset instantiator cannot replace call
+[instantiate] tests/string/memset_0.c:68: Warning: 
+  memset instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
index 91a1e42f767..137dd1c21a0 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
@@ -1,8 +1,12 @@
 [kernel] Parsing tests/string/memset_FF.c (with preprocessing)
-[instantiate] tests/string/memset_FF.c:88: Warning: Ignore call: not well typed
-[instantiate] tests/string/memset_FF.c:89: Warning: Ignore call: not well typed
-[instantiate] tests/string/memset_FF.c:93: Warning: Ignore call: not well typed
-[instantiate] tests/string/memset_FF.c:94: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_FF.c:88: Warning: 
+  memset instantiator cannot replace call
+[instantiate] tests/string/memset_FF.c:89: Warning: 
+  memset instantiator cannot replace call
+[instantiate] tests/string/memset_FF.c:93: Warning: 
+  memset instantiator cannot replace call
+[instantiate] tests/string/memset_FF.c:94: Warning: 
+  memset instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle
index f71268da3aa..7185fe7a665 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle
@@ -1,6 +1,6 @@
 [kernel] Parsing tests/string/memset_nested_union.c (with preprocessing)
 [instantiate] tests/string/memset_nested_union.c:10: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
index 8609a955121..5ece8370f6b 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
@@ -1,40 +1,40 @@
 [kernel] Parsing tests/string/memset_value.c (with preprocessing)
 [instantiate] tests/string/memset_value.c:26: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:27: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:32: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:33: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:37: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:38: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:42: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:43: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:47: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:48: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:52: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:53: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:57: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:58: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:62: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:63: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:67: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 [instantiate] tests/string/memset_value.c:68: Warning: 
-  Ignore call: not well typed
+  memset instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
diff --git a/src/plugins/instantiate/transform.ml b/src/plugins/instantiate/transform.ml
index 8b0f9ece40e..7dda9a46b99 100644
--- a/src/plugins/instantiate/transform.ml
+++ b/src/plugins/instantiate/transform.ml
@@ -99,7 +99,8 @@ class transformer = object(self)
         Queue.add fundec used_instantiator_last_kf ;
         (fundec.svar), new_args
       else begin
-        Options.warning ~current:true "Ignore call: not well typed" ;
+        Options.warning
+          ~current:true "%s instantiator cannot replace call" fct.vname ;
         (fct, args)
       end
     with
-- 
GitLab