diff --git a/src/plugins/instantiate/Instantiate.mli b/src/plugins/instantiate/Instantiate.mli index 4af9d03fc532db1fd1983060eace584d6f010aa1..aaddb8131d05730a789bf344b1df2497912ae093 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 fca57bd58d0ed47e5acccb5cb39bbe5fd55a12c8..a6bbb923b7c7a39ff64c7ce5233de5abb414d4a1 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 cc72848fd620f5aee8c2dce2f91fa4e145383d34..1670641826813ce9b10d06d60f85849cf9e55a57 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 cfdb769ed8d5e5412d854f0a741ba18d912fcfaf..a0671fe0bc81d0cf757f8660830d2cf9ab1898c8 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 6cec0abadff6e4e4fd12bfb6d6629c04e09816a6..9aff502467ca08d49dc7d2f346e2e05c6894c995 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 856300f9ad02c6ada927f4ccc39d1f04c436be7b..1f82bcd57b000001f672deb6a8e1f9f34dd3f699 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 35a4b88ca8fc95e3b60b3bd9ab6af8c41c3a50d3..899dd8afefc6053b12a354ddcec1ba03c5f71842 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 b53227bdabf4910160b6a2ba74c014ef788e3ea5..f327581499bdc3f2393d4bd573a08d587761e1df 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 af6a60f7c80cf3156dafa841eacb02efbb0e2002..dae2db7eba374181cfa6fe5705cbcd211dfeaed5 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 91a1e42f767e8b671d559e1c81df16766352659e..137dd1c21a070c374f27367c3e82beb2b47a79aa 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 f71268da3aab3046b86c67795177069ebc7de2f2..7185fe7a66598d4ad182720f927ea6e5f4ed4a8b 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 8609a955121da6329d80d472a6c6283008fd558b..5ece8370f6baf098afc773974cb82a40f53df732 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 8b0f9ece40e0e65732f1f6dddf2192946d56d692..7dda9a46b9960f41b5e10742a2f5c7669b85d3b9 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