From 9c137e93b9e6f66085e0a16a0616ddcabf4747cd Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 2 Oct 2020 11:13:34 +0200
Subject: [PATCH] adds src/plugins/instantiate/tests
---
Makefile | 2 +-
.../instantiate/tests/plugin/needs_global.i | 3 ++-
.../tests/stdlib/oracle/calloc.res.oracle | 8 +++---
.../tests/stdlib/oracle/free.res.oracle | 5 ++--
.../tests/stdlib/oracle/malloc.res.oracle | 8 +++---
.../stdlib/oracle/no_fc_stdlib.res.oracle | 2 +-
.../tests/string/oracle/memcmp.res.oracle | 20 +++++---------
.../tests/string/oracle/memcpy.res.oracle | 26 +++++++------------
.../tests/string/oracle/memmove.res.oracle | 26 +++++++------------
.../tests/string/oracle/memset_0.res.oracle | 14 ++++------
.../tests/string/oracle/memset_FF.res.oracle | 14 ++++------
.../oracle/memset_nested_typedef.res.oracle | 2 +-
.../oracle/memset_nested_union.res.oracle | 2 +-
.../string/oracle/memset_value.res.oracle | 2 +-
14 files changed, 50 insertions(+), 84 deletions(-)
diff --git a/Makefile b/Makefile
index 3c85017583b..7c66be80e3d 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 dfd53797477..245a6045b87 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 73c1498972e..29b8fdd24bf 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 455c27b6a98..38e7d9ff738 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 937ab718ace..988a5aeae15 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 aee7a0a4fdc..ecaf57dd077 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 ec0ea5d3ff7..0aefc17a642 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 aec6333d51e..40671d2df88 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 79fa2042f49..9bea14b825c 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 87d59684722..94828ff53e5 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 0a28fe5684d..5521423c1b2 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 3c594189ca2..9ed88a529d8 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 786600053d5..c8f55a2befb 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 177c58404d0..649276af370 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"
--
GitLab