diff --git a/Makefile b/Makefile index 3c85017583b9d5b5652ad7847e3f5cb23fc3a6fe..7c66be80e3d66a587ce9a3482fdf913cc75b9ba2 100644 --- a/Makefile +++ b/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 diff --git a/src/plugins/instantiate/tests/plugin/needs_global.i b/src/plugins/instantiate/tests/plugin/needs_global.i index dfd53797477e08a50c44b80b06ea9743a7a73614..245a6045b8777792b6df4568fc4a440ce6ad65b7 100644 --- a/src/plugins/instantiate/tests/plugin/needs_global.i +++ b/src/plugins/instantiate/tests/plugin/needs_global.i @@ -1,5 +1,6 @@ /* 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 diff --git a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle index 73c1498972eac7cdaf9affea19ccbfc5f6903636..29b8fdd24bf84252e3020ae64d0681783769ae8d 100644 --- a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle +++ b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle @@ -1,8 +1,6 @@ [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 { diff --git a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle index 455c27b6a98530988e06ac0585ca54a8ea15f4bb..38e7d9ff738d4e42abc3f59ddbbb158114e54c3d 100644 --- a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle +++ b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle @@ -1,6 +1,5 @@ [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; diff --git a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle index 937ab718ace93b2d0e91d24d73367cffb936f06b..988a5aeae159b8f41b8b1473947f5b00dfe6fc67 100644 --- a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle +++ b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle @@ -1,8 +1,6 @@ [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 { diff --git a/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle index aee7a0a4fdc5b083076af980562bc464a9171c7d..ecaf57dd07748e3d2b8f14de95ba2b3ff5fe6756 100644 --- a/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle +++ b/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; */ diff --git a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle index ec0ea5d3ff779444bc906bf30e41545d298e7bde..0aefc17a642399c76faabbaa837b5069fe62dd57 100644 --- a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle +++ b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle @@ -1,16 +1,10 @@ [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" diff --git a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle index aec6333d51edd826799748124a5e661e609f319d..40671d2df8840e9665a4a13a03b596a53b97f8de 100644 --- a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle +++ b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle @@ -1,20 +1,12 @@ [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" diff --git a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle index 79fa2042f4975c3c9718388c6f26e5579c3837e7..9bea14b825cb9c3d81775f5b84212031c3e6591e 100644 --- a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle +++ b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle @@ -1,20 +1,12 @@ [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" 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 87d596847226c1a08122de3ad13722b557424c56..94828ff53e511ca8bdbf0fabda3b6c771b815506 100644 --- a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle +++ b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle @@ -1,12 +1,8 @@ [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" 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 0a28fe5684dd0710646493b9378667057b6e2a8a..5521423c1b2117d7a99e1563dccc017170835b1f 100644 --- a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle +++ b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle @@ -1,12 +1,8 @@ [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" diff --git a/src/plugins/instantiate/tests/string/oracle/memset_nested_typedef.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_nested_typedef.res.oracle index 3c594189ca236343fded4ffd1a75972eb87fb914..9ed88a529d86d0855e3a05d27f1c3989666a9bda 100644 --- a/src/plugins/instantiate/tests/string/oracle/memset_nested_typedef.res.oracle +++ b/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" 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 786600053d5a15c5fa6484b2155d4aa2872e358d..c8f55a2befb06d5e1b067b5ca928704fce845aa4 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 @@ -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" 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 177c58404d0c369fe1a5c5aa6b4cfcbc34acc1ba..649276af3705a37ee10c86a6c81581729b9bade3 100644 --- a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle +++ b/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"