adds src/plugins/instantiate/tests

Makefile

@@ -170,7 +170,7 @@ force-reconfigure:
 
 TESTS=builtins callgraph cil constant_propagation float idct impact jcdb journal libc metrics misc occurrence pdg rte rte_manual scope slicing sparecode spec syntax test value
 
-PLUGIN_TESTS= dive loop_analysis markdown-report nonterm server variadic
+PLUGIN_TESTS= dive instantiate loop_analysis markdown-report nonterm server variadic
 
 tests: config.sed
 	find tests $(addprefix src/plugins/,$(addsuffix /tests,$(PLUGIN_TESTS))) -name dune | grep -e "oracle.*/\|result.*/" | xargs --no-run-if-empty rm

src/plugins/instantiate/tests/plugin/needs_global.i

 /* run.config
-   OPT: -load-script tests/plugin/needs_globals.ml -instantiate -check -print
+   MODULE: needs_globals.cmxs
+   OPT: -instantiate -check -print
 */
 
 int i ; // needed for already_one specifciation

src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle

 [kernel] Parsing calloc.c (with preprocessing)
-[instantiate] calloc.c:24: Warning: 
-  calloc instantiator cannot replace call
-[instantiate] calloc.c:25: Warning: 
-  calloc instantiator cannot replace call
+[instantiate] calloc.c:24: Warning: calloc instantiator cannot replace call
+[instantiate] calloc.c:25: Warning: calloc instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stdlib.h"
 struct X {
@@ -316,7 +314,7 @@ int main(void)
 }
 
 
-[kernel] Parsing result/calloc.c (with preprocessing)
+[kernel] Parsing ocode_0_calloc.c (with preprocessing)
 /* Generated by Frama-C */
 #include "stdlib.h"
 struct X {

src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle

 [kernel] Parsing free.c (with preprocessing)
-[instantiate] free.c:13: Warning: 
-  free instantiator cannot replace call
+[instantiate] free.c:13: Warning: free instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stdlib.h"
 struct incomplete;
@@ -139,7 +138,7 @@ void with_incomplete(struct incomplete *t)
 }
 
 
-[kernel] Parsing result/free.c (with preprocessing)
+[kernel] Parsing ocode_0_free.c (with preprocessing)
 /* Generated by Frama-C */
 #include "stdlib.h"
 struct incomplete;

src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle

 [kernel] Parsing malloc.c (with preprocessing)
-[instantiate] malloc.c:23: Warning: 
-  malloc instantiator cannot replace call
-[instantiate] malloc.c:24: Warning: 
-  malloc instantiator cannot replace call
+[instantiate] malloc.c:23: Warning: malloc instantiator cannot replace call
+[instantiate] malloc.c:24: Warning: malloc instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stdlib.h"
 struct X {
@@ -218,7 +216,7 @@ int main(void)
 }
 
 
-[kernel] Parsing result/malloc.c (with preprocessing)
+[kernel] Parsing ocode_0_malloc.c (with preprocessing)
 /* Generated by Frama-C */
 #include "stdlib.h"
 struct X {

src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle

@@ -124,7 +124,7 @@ void foo(void)
 }
 
 
-[kernel] Parsing result/no_fc_stdlib.c (with preprocessing)
+[kernel] Parsing ocode_0_no_fc_stdlib.c (with preprocessing)
 /* Generated by Frama-C */
 #include "stddef.h"
 /*@ ghost extern int __fc_heap_status; */

src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle

 [kernel] Parsing memcmp.c (with preprocessing)
-[instantiate] memcmp.c:31: Warning: 
-  memcmp instantiator cannot replace call
-[instantiate] memcmp.c:36: Warning: 
-  memcmp instantiator cannot replace call
-[instantiate] memcmp.c:40: Warning: 
-  memcmp instantiator cannot replace call
-[instantiate] memcmp.c:41: Warning: 
-  memcmp instantiator cannot replace call
-[instantiate] memcmp.c:42: Warning: 
-  memcmp instantiator cannot replace call
-[instantiate] memcmp.c:43: Warning: 
-  memcmp instantiator cannot replace call
+[instantiate] memcmp.c:31: Warning: memcmp instantiator cannot replace call
+[instantiate] memcmp.c:36: Warning: memcmp instantiator cannot replace call
+[instantiate] memcmp.c:40: Warning: memcmp instantiator cannot replace call
+[instantiate] memcmp.c:41: Warning: memcmp instantiator cannot replace call
+[instantiate] memcmp.c:42: Warning: memcmp instantiator cannot replace call
+[instantiate] memcmp.c:43: Warning: memcmp instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
@@ -181,7 +175,7 @@ void with_null_or_int(int * /*[10]*/ p)
 }
 
 
-[kernel] Parsing result/memcmp.c (with preprocessing)
+[kernel] Parsing ocode_0_memcmp.c (with preprocessing)
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"

src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle

 [kernel] Parsing memcpy.c (with preprocessing)
-[instantiate] memcpy.c:36: Warning: 
-  memcpy instantiator cannot replace call
-[instantiate] memcpy.c:37: Warning: 
-  memcpy instantiator cannot replace call
-[instantiate] memcpy.c:42: Warning: 
-  memcpy instantiator cannot replace call
-[instantiate] memcpy.c:43: Warning: 
-  memcpy instantiator cannot replace call
-[instantiate] memcpy.c:47: Warning: 
-  memcpy instantiator cannot replace call
-[instantiate] memcpy.c:48: Warning: 
-  memcpy instantiator cannot replace call
-[instantiate] memcpy.c:49: Warning: 
-  memcpy instantiator cannot replace call
-[instantiate] memcpy.c:50: Warning: 
-  memcpy instantiator cannot replace call
+[instantiate] memcpy.c:36: Warning: memcpy instantiator cannot replace call
+[instantiate] memcpy.c:37: Warning: memcpy instantiator cannot replace call
+[instantiate] memcpy.c:42: Warning: memcpy instantiator cannot replace call
+[instantiate] memcpy.c:43: Warning: memcpy instantiator cannot replace call
+[instantiate] memcpy.c:47: Warning: memcpy instantiator cannot replace call
+[instantiate] memcpy.c:48: Warning: memcpy instantiator cannot replace call
+[instantiate] memcpy.c:49: Warning: memcpy instantiator cannot replace call
+[instantiate] memcpy.c:50: Warning: memcpy instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
@@ -195,7 +187,7 @@ void with_null_or_int(int * /*[10]*/ p)
 }
 
 
-[kernel] Parsing result/memcpy.c (with preprocessing)
+[kernel] Parsing ocode_0_memcpy.c (with preprocessing)
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"

src/plugins/instantiate/tests/string/oracle/memmove.res.oracle

 [kernel] Parsing memmove.c (with preprocessing)
-[instantiate] memmove.c:36: Warning: 
-  memmove instantiator cannot replace call
-[instantiate] memmove.c:37: Warning: 
-  memmove instantiator cannot replace call
-[instantiate] memmove.c:42: Warning: 
-  memmove instantiator cannot replace call
-[instantiate] memmove.c:43: Warning: 
-  memmove instantiator cannot replace call
-[instantiate] memmove.c:47: Warning: 
-  memmove instantiator cannot replace call
-[instantiate] memmove.c:48: Warning: 
-  memmove instantiator cannot replace call
-[instantiate] memmove.c:49: Warning: 
-  memmove instantiator cannot replace call
-[instantiate] memmove.c:50: Warning: 
-  memmove instantiator cannot replace call
+[instantiate] memmove.c:36: Warning: memmove instantiator cannot replace call
+[instantiate] memmove.c:37: Warning: memmove instantiator cannot replace call
+[instantiate] memmove.c:42: Warning: memmove instantiator cannot replace call
+[instantiate] memmove.c:43: Warning: memmove instantiator cannot replace call
+[instantiate] memmove.c:47: Warning: memmove instantiator cannot replace call
+[instantiate] memmove.c:48: Warning: memmove instantiator cannot replace call
+[instantiate] memmove.c:49: Warning: memmove instantiator cannot replace call
+[instantiate] memmove.c:50: Warning: memmove instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
@@ -179,7 +171,7 @@ void with_null_or_int(int * /*[10]*/ p)
 }
 
 
-[kernel] Parsing result/memmove.c (with preprocessing)
+[kernel] Parsing ocode_0_memmove.c (with preprocessing)
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"

src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle

 [kernel] Parsing memset_0.c (with preprocessing)
-[instantiate] memset_0.c:62: Warning: 
-  memset instantiator cannot replace call
-[instantiate] memset_0.c:63: Warning: 
-  memset instantiator cannot replace call
-[instantiate] memset_0.c:67: Warning: 
-  memset instantiator cannot replace call
-[instantiate] memset_0.c:68: Warning: 
-  memset instantiator cannot replace call
+[instantiate] memset_0.c:62: Warning: memset instantiator cannot replace call
+[instantiate] memset_0.c:63: Warning: memset instantiator cannot replace call
+[instantiate] memset_0.c:67: Warning: memset instantiator cannot replace call
+[instantiate] memset_0.c:68: Warning: memset instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
@@ -278,7 +274,7 @@ void with_null_or_int(void)
 }
 
 
-[kernel] Parsing result/memset_0.c (with preprocessing)
+[kernel] Parsing ocode_0_memset_0.c (with preprocessing)
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"

src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle

 [kernel] Parsing memset_FF.c (with preprocessing)
-[instantiate] memset_FF.c:88: Warning: 
-  memset instantiator cannot replace call
-[instantiate] memset_FF.c:89: Warning: 
-  memset instantiator cannot replace call
-[instantiate] memset_FF.c:93: Warning: 
-  memset instantiator cannot replace call
-[instantiate] memset_FF.c:94: Warning: 
-  memset instantiator cannot replace call
+[instantiate] memset_FF.c:88: Warning: memset instantiator cannot replace call
+[instantiate] memset_FF.c:89: Warning: memset instantiator cannot replace call
+[instantiate] memset_FF.c:93: Warning: memset instantiator cannot replace call
+[instantiate] memset_FF.c:94: Warning: memset instantiator cannot replace call
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
@@ -415,7 +411,7 @@ void with_null_or_int(void)
 }
 
 
-[kernel] Parsing result/memset_FF.c (with preprocessing)
+[kernel] Parsing ocode_0_memset_FF.c (with preprocessing)
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"

src/plugins/instantiate/tests/string/oracle/memset_nested_typedef.res.oracle

@@ -34,7 +34,7 @@ void test(void)
 }
 
 
-[kernel] Parsing result/memset_nested_typedef.c (with preprocessing)
+[kernel] Parsing ocode_0_memset_nested_typedef.c (with preprocessing)
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"

src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle

@@ -20,7 +20,7 @@ void test(void)
 }
 
 
-[kernel] Parsing result/memset_nested_union.c (with preprocessing)
+[kernel] Parsing ocode_0_memset_nested_union.c (with preprocessing)
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"

src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle

@@ -191,7 +191,7 @@ void with_null_or_int(int value)
 }
 
 
-[kernel] Parsing result/memset_value.c (with preprocessing)
+[kernel] Parsing ocode_0_memset_value.c (with preprocessing)
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"