diff --git a/headers/header_spec.txt b/headers/header_spec.txt index 093fdc6dc8718b8b1758418877691e94bcc136d1..7eb1cb9bbecde3b4a4b0f566ca13c4a3e24b7b63 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -937,16 +937,16 @@ src/plugins/builtin/builtin_builder.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/builtin/builtin_builder.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/builtin/configure.ac: CEA_LGPL_OR_PROPRIETARY src/plugins/builtin/Makefile.in: CEA_LGPL_OR_PROPRIETARY -src/plugins/builtin/malloc.ml: CEA_LGPL_OR_PROPRIETARY -src/plugins/builtin/malloc.mli: CEA_LGPL_OR_PROPRIETARY -src/plugins/builtin/memcmp.ml: CEA_LGPL_OR_PROPRIETARY -src/plugins/builtin/memcmp.mli: CEA_LGPL_OR_PROPRIETARY -src/plugins/builtin/memcpy.ml: CEA_LGPL_OR_PROPRIETARY -src/plugins/builtin/memcpy.mli: CEA_LGPL_OR_PROPRIETARY -src/plugins/builtin/memmove.ml: CEA_LGPL_OR_PROPRIETARY -src/plugins/builtin/memmove.mli: CEA_LGPL_OR_PROPRIETARY -src/plugins/builtin/memset.ml: CEA_LGPL_OR_PROPRIETARY -src/plugins/builtin/memset.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/builtin/stdlib/malloc.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/builtin/stdlib/malloc.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/builtin/string/memcmp.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/builtin/string/memcmp.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/builtin/string/memcpy.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/builtin/string/memcpy.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/builtin/string/memmove.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/builtin/string/memmove.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/builtin/string/memset.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/builtin/string/memset.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/builtin/options.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/builtin/options.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/builtin/register.ml: CEA_LGPL_OR_PROPRIETARY diff --git a/src/plugins/builtin/Makefile.in b/src/plugins/builtin/Makefile.in index 09306b9c327adafd9a81c91d28e99c60a3a94a2d..ec3691bfd99f7088ed4cb08aea4e580651e6ad49 100644 --- a/src/plugins/builtin/Makefile.in +++ b/src/plugins/builtin/Makefile.in @@ -29,6 +29,17 @@ ifndef FRAMAC_LIBDIR FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath) endif +SRC_STRING:= \ + memcpy \ + memcmp \ + memmove \ + memset +SRC_STRING:=$(addprefix string/, $(SRC_STRING)) + +SRC_STDLIB:= \ + malloc +SRC_STDLIB:=$(addprefix stdlib/, $(SRC_STDLIB)) + ################### # Plug-in Setting # ################### @@ -36,14 +47,19 @@ endif PLUGIN_DIR ?= . PLUGIN_ENABLE := @ENABLE_BUILTIN@ PLUGIN_NAME := Builtin +PLUGIN_EXTRA_DIRS:=\ + string\ + stdlib PLUGIN_CMI := -PLUGIN_CMO := basic_blocks options builtin_builder transform \ - malloc memcpy memcmp memmove memset \ - register +PLUGIN_CMO := \ + basic_blocks options builtin_builder transform register \ + $(SRC_STRING) \ + $(SRC_STDLIB) + PLUGIN_DISTRIBUTED := $(PLUGIN_ENABLE) PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure #PLUGIN_NO_DEFAULT_TEST := no -PLUGIN_TESTS_DIRS := functions options +PLUGIN_TESTS_DIRS := string options ################ # Generic part # diff --git a/src/plugins/builtin/malloc.ml b/src/plugins/builtin/stdlib/malloc.ml similarity index 100% rename from src/plugins/builtin/malloc.ml rename to src/plugins/builtin/stdlib/malloc.ml diff --git a/src/plugins/builtin/malloc.mli b/src/plugins/builtin/stdlib/malloc.mli similarity index 100% rename from src/plugins/builtin/malloc.mli rename to src/plugins/builtin/stdlib/malloc.mli diff --git a/src/plugins/builtin/memcmp.ml b/src/plugins/builtin/string/memcmp.ml similarity index 100% rename from src/plugins/builtin/memcmp.ml rename to src/plugins/builtin/string/memcmp.ml diff --git a/src/plugins/builtin/memcmp.mli b/src/plugins/builtin/string/memcmp.mli similarity index 100% rename from src/plugins/builtin/memcmp.mli rename to src/plugins/builtin/string/memcmp.mli diff --git a/src/plugins/builtin/memcpy.ml b/src/plugins/builtin/string/memcpy.ml similarity index 100% rename from src/plugins/builtin/memcpy.ml rename to src/plugins/builtin/string/memcpy.ml diff --git a/src/plugins/builtin/memcpy.mli b/src/plugins/builtin/string/memcpy.mli similarity index 100% rename from src/plugins/builtin/memcpy.mli rename to src/plugins/builtin/string/memcpy.mli diff --git a/src/plugins/builtin/memmove.ml b/src/plugins/builtin/string/memmove.ml similarity index 100% rename from src/plugins/builtin/memmove.ml rename to src/plugins/builtin/string/memmove.ml diff --git a/src/plugins/builtin/memmove.mli b/src/plugins/builtin/string/memmove.mli similarity index 100% rename from src/plugins/builtin/memmove.mli rename to src/plugins/builtin/string/memmove.mli diff --git a/src/plugins/builtin/memset.ml b/src/plugins/builtin/string/memset.ml similarity index 100% rename from src/plugins/builtin/memset.ml rename to src/plugins/builtin/string/memset.ml diff --git a/src/plugins/builtin/memset.mli b/src/plugins/builtin/string/memset.mli similarity index 100% rename from src/plugins/builtin/memset.mli rename to src/plugins/builtin/string/memset.mli diff --git a/src/plugins/builtin/tests/functions/memcmp.c b/src/plugins/builtin/tests/string/memcmp.c similarity index 100% rename from src/plugins/builtin/tests/functions/memcmp.c rename to src/plugins/builtin/tests/string/memcmp.c diff --git a/src/plugins/builtin/tests/functions/memcpy.c b/src/plugins/builtin/tests/string/memcpy.c similarity index 100% rename from src/plugins/builtin/tests/functions/memcpy.c rename to src/plugins/builtin/tests/string/memcpy.c diff --git a/src/plugins/builtin/tests/functions/memmove.c b/src/plugins/builtin/tests/string/memmove.c similarity index 100% rename from src/plugins/builtin/tests/functions/memmove.c rename to src/plugins/builtin/tests/string/memmove.c diff --git a/src/plugins/builtin/tests/functions/memset_0.c b/src/plugins/builtin/tests/string/memset_0.c similarity index 100% rename from src/plugins/builtin/tests/functions/memset_0.c rename to src/plugins/builtin/tests/string/memset_0.c diff --git a/src/plugins/builtin/tests/functions/memset_FF.c b/src/plugins/builtin/tests/string/memset_FF.c similarity index 100% rename from src/plugins/builtin/tests/functions/memset_FF.c rename to src/plugins/builtin/tests/string/memset_FF.c diff --git a/src/plugins/builtin/tests/functions/memset_value.c b/src/plugins/builtin/tests/string/memset_value.c similarity index 100% rename from src/plugins/builtin/tests/functions/memset_value.c rename to src/plugins/builtin/tests/string/memset_value.c diff --git a/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle b/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle similarity index 85% rename from src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle rename to src/plugins/builtin/tests/string/oracle/memcmp.res.oracle index b0d88d0280a155addeb1e1fb960868b71896202d..646b873e44cdacc2c02d7405e20ce67f34e1619c 100644 --- a/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle +++ b/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle @@ -1,4 +1,4 @@ -[kernel] Parsing tests/functions/memcmp.c (with preprocessing) +[kernel] Parsing tests/string/memcmp.c (with preprocessing) /* Generated by Frama-C */ #include "stddef.h" #include "string.h" @@ -143,18 +143,18 @@ int nested(int (*src)[10], int (*dest)[10], int n) } -[kernel] Parsing tests/functions/result/memcmp.c (with preprocessing) -[kernel] Parsing tests/functions/memcmp.c (with preprocessing) -[kernel] tests/functions/memcmp.c:10: Warning: - def'n of func integer at tests/functions/memcmp.c:10 (sum 1085) conflicts with the one at tests/functions/result/memcmp.c:34 (sum 1972); keeping the one at tests/functions/result/memcmp.c:34. -[kernel] tests/functions/memcmp.c:14: Warning: - def'n of func with_named at tests/functions/memcmp.c:14 (sum 1085) conflicts with the one at tests/functions/result/memcmp.c:41 (sum 1972); keeping the one at tests/functions/result/memcmp.c:41. -[kernel] tests/functions/memcmp.c:18: Warning: - def'n of func structure at tests/functions/memcmp.c:18 (sum 1085) conflicts with the one at tests/functions/result/memcmp.c:72 (sum 1972); keeping the one at tests/functions/result/memcmp.c:72. -[kernel] tests/functions/memcmp.c:22: Warning: - def'n of func pointers at tests/functions/memcmp.c:22 (sum 1085) conflicts with the one at tests/functions/result/memcmp.c:103 (sum 1972); keeping the one at tests/functions/result/memcmp.c:103. -[kernel] tests/functions/memcmp.c:26: Warning: - def'n of func nested at tests/functions/memcmp.c:26 (sum 1087) conflicts with the one at tests/functions/result/memcmp.c:137 (sum 1974); keeping the one at tests/functions/result/memcmp.c:137. +[kernel] Parsing tests/string/result/memcmp.c (with preprocessing) +[kernel] Parsing tests/string/memcmp.c (with preprocessing) +[kernel] tests/string/memcmp.c:10: Warning: + def'n of func integer at tests/string/memcmp.c:10 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:34 (sum 1972); keeping the one at tests/string/result/memcmp.c:34. +[kernel] tests/string/memcmp.c:14: Warning: + def'n of func with_named at tests/string/memcmp.c:14 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:41 (sum 1972); keeping the one at tests/string/result/memcmp.c:41. +[kernel] tests/string/memcmp.c:18: Warning: + def'n of func structure at tests/string/memcmp.c:18 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:72 (sum 1972); keeping the one at tests/string/result/memcmp.c:72. +[kernel] tests/string/memcmp.c:22: Warning: + def'n of func pointers at tests/string/memcmp.c:22 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:103 (sum 1972); keeping the one at tests/string/result/memcmp.c:103. +[kernel] tests/string/memcmp.c:26: Warning: + def'n of func nested at tests/string/memcmp.c:26 (sum 1087) conflicts with the one at tests/string/result/memcmp.c:137 (sum 1974); keeping the one at tests/string/result/memcmp.c:137. /* Generated by Frama-C */ #include "stddef.h" #include "string.h" diff --git a/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle b/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle similarity index 90% rename from src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle rename to src/plugins/builtin/tests/string/oracle/memcpy.res.oracle index b29798e2515dc29fe898a22bc591785a030c417c..4a9d9e029c0b5f0489388b072c0867e0ba5f49f1 100644 --- a/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle +++ b/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle @@ -1,4 +1,4 @@ -[kernel] Parsing tests/functions/memcpy.c (with preprocessing) +[kernel] Parsing tests/string/memcpy.c (with preprocessing) /* Generated by Frama-C */ #include "stddef.h" #include "string.h" @@ -154,18 +154,18 @@ void nested(int (*src)[10], int (*dest)[10], int n) } -[kernel] Parsing tests/functions/result/memcpy.c (with preprocessing) -[kernel] Parsing tests/functions/memcpy.c (with preprocessing) -[kernel] tests/functions/memcpy.c:10: Warning: - dropping duplicate def'n of func integer at tests/functions/memcpy.c:10 in favor of that at tests/functions/result/memcpy.c:36 -[kernel] tests/functions/memcpy.c:15: Warning: - dropping duplicate def'n of func with_named at tests/functions/memcpy.c:15 in favor of that at tests/functions/result/memcpy.c:43 -[kernel] tests/functions/memcpy.c:20: Warning: - dropping duplicate def'n of func structure at tests/functions/memcpy.c:20 in favor of that at tests/functions/result/memcpy.c:76 -[kernel] tests/functions/memcpy.c:25: Warning: - dropping duplicate def'n of func pointers at tests/functions/memcpy.c:25 in favor of that at tests/functions/result/memcpy.c:109 -[kernel] tests/functions/memcpy.c:30: Warning: - dropping duplicate def'n of func nested at tests/functions/memcpy.c:30 in favor of that at tests/functions/result/memcpy.c:147 +[kernel] Parsing tests/string/result/memcpy.c (with preprocessing) +[kernel] Parsing tests/string/memcpy.c (with preprocessing) +[kernel] tests/string/memcpy.c:10: Warning: + dropping duplicate def'n of func integer at tests/string/memcpy.c:10 in favor of that at tests/string/result/memcpy.c:36 +[kernel] tests/string/memcpy.c:15: Warning: + dropping duplicate def'n of func with_named at tests/string/memcpy.c:15 in favor of that at tests/string/result/memcpy.c:43 +[kernel] tests/string/memcpy.c:20: Warning: + dropping duplicate def'n of func structure at tests/string/memcpy.c:20 in favor of that at tests/string/result/memcpy.c:76 +[kernel] tests/string/memcpy.c:25: Warning: + dropping duplicate def'n of func pointers at tests/string/memcpy.c:25 in favor of that at tests/string/result/memcpy.c:109 +[kernel] tests/string/memcpy.c:30: Warning: + dropping duplicate def'n of func nested at tests/string/memcpy.c:30 in favor of that at tests/string/result/memcpy.c:147 /* Generated by Frama-C */ #include "stddef.h" #include "string.h" diff --git a/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle b/src/plugins/builtin/tests/string/oracle/memmove.res.oracle similarity index 88% rename from src/plugins/builtin/tests/functions/oracle/memmove.res.oracle rename to src/plugins/builtin/tests/string/oracle/memmove.res.oracle index 43e53fcefa4d1ae98f9c3c82d4cb6697452715e2..b85ede266e4f6cc8519bc08c84a4abcaf3ebf16d 100644 --- a/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle +++ b/src/plugins/builtin/tests/string/oracle/memmove.res.oracle @@ -1,4 +1,4 @@ -[kernel] Parsing tests/functions/memmove.c (with preprocessing) +[kernel] Parsing tests/string/memmove.c (with preprocessing) /* Generated by Frama-C */ #include "stddef.h" #include "string.h" @@ -138,18 +138,18 @@ void nested(int (*src)[10], int (*dest)[10], int n) } -[kernel] Parsing tests/functions/result/memmove.c (with preprocessing) -[kernel] Parsing tests/functions/memmove.c (with preprocessing) -[kernel] tests/functions/memmove.c:10: Warning: - dropping duplicate def'n of func integer at tests/functions/memmove.c:10 in favor of that at tests/functions/result/memmove.c:32 -[kernel] tests/functions/memmove.c:15: Warning: - dropping duplicate def'n of func with_named at tests/functions/memmove.c:15 in favor of that at tests/functions/result/memmove.c:39 -[kernel] tests/functions/memmove.c:20: Warning: - dropping duplicate def'n of func structure at tests/functions/memmove.c:20 in favor of that at tests/functions/result/memmove.c:68 -[kernel] tests/functions/memmove.c:25: Warning: - dropping duplicate def'n of func pointers at tests/functions/memmove.c:25 in favor of that at tests/functions/result/memmove.c:97 -[kernel] tests/functions/memmove.c:30: Warning: - dropping duplicate def'n of func nested at tests/functions/memmove.c:30 in favor of that at tests/functions/result/memmove.c:131 +[kernel] Parsing tests/string/result/memmove.c (with preprocessing) +[kernel] Parsing tests/string/memmove.c (with preprocessing) +[kernel] tests/string/memmove.c:10: Warning: + dropping duplicate def'n of func integer at tests/string/memmove.c:10 in favor of that at tests/string/result/memmove.c:32 +[kernel] tests/string/memmove.c:15: Warning: + dropping duplicate def'n of func with_named at tests/string/memmove.c:15 in favor of that at tests/string/result/memmove.c:39 +[kernel] tests/string/memmove.c:20: Warning: + dropping duplicate def'n of func structure at tests/string/memmove.c:20 in favor of that at tests/string/result/memmove.c:68 +[kernel] tests/string/memmove.c:25: Warning: + dropping duplicate def'n of func pointers at tests/string/memmove.c:25 in favor of that at tests/string/result/memmove.c:97 +[kernel] tests/string/memmove.c:30: Warning: + dropping duplicate def'n of func nested at tests/string/memmove.c:30 in favor of that at tests/string/result/memmove.c:131 /* Generated by Frama-C */ #include "stddef.h" #include "string.h" diff --git a/src/plugins/builtin/tests/functions/oracle/memset_0.res.oracle b/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle similarity index 87% rename from src/plugins/builtin/tests/functions/oracle/memset_0.res.oracle rename to src/plugins/builtin/tests/string/oracle/memset_0.res.oracle index 19daa1257c9aa01eab0e200c4286918cc5830849..5dcae838d7dd04eacab54332a8f43f02dd841cbf 100644 --- a/src/plugins/builtin/tests/functions/oracle/memset_0.res.oracle +++ b/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle @@ -1,4 +1,4 @@ -[kernel] Parsing tests/functions/memset_0.c (with preprocessing) +[kernel] Parsing tests/string/memset_0.c (with preprocessing) /* Generated by Frama-C */ #include "stddef.h" #include "string.h" @@ -225,26 +225,26 @@ void nested(int (*dest)[10], int n) } -[kernel] Parsing tests/functions/result/memset_0.c (with preprocessing) -[kernel] Parsing tests/functions/memset_0.c (with preprocessing) -[kernel] tests/functions/memset_0.c:10: Warning: - dropping duplicate def'n of func chars at tests/functions/memset_0.c:10 in favor of that at tests/functions/result/memset_0.c:26 -[kernel] tests/functions/memset_0.c:15: Warning: - dropping duplicate def'n of func uchars at tests/functions/memset_0.c:15 in favor of that at tests/functions/result/memset_0.c:50 -[kernel] tests/functions/memset_0.c:20: Warning: - dropping duplicate def'n of func nested_chars at tests/functions/memset_0.c:20 in favor of that at tests/functions/result/memset_0.c:78 -[kernel] tests/functions/memset_0.c:25: Warning: - dropping duplicate def'n of func integer at tests/functions/memset_0.c:25 in favor of that at tests/functions/result/memset_0.c:104 -[kernel] tests/functions/memset_0.c:30: Warning: - dropping duplicate def'n of func floats at tests/functions/memset_0.c:30 in favor of that at tests/functions/result/memset_0.c:130 -[kernel] tests/functions/memset_0.c:35: Warning: - dropping duplicate def'n of func with_named at tests/functions/memset_0.c:35 in favor of that at tests/functions/result/memset_0.c:137 -[kernel] tests/functions/memset_0.c:40: Warning: - dropping duplicate def'n of func structure at tests/functions/memset_0.c:40 in favor of that at tests/functions/result/memset_0.c:164 -[kernel] tests/functions/memset_0.c:45: Warning: - dropping duplicate def'n of func pointers at tests/functions/memset_0.c:45 in favor of that at tests/functions/result/memset_0.c:190 -[kernel] tests/functions/memset_0.c:50: Warning: - dropping duplicate def'n of func nested at tests/functions/memset_0.c:50 in favor of that at tests/functions/result/memset_0.c:218 +[kernel] Parsing tests/string/result/memset_0.c (with preprocessing) +[kernel] Parsing tests/string/memset_0.c (with preprocessing) +[kernel] tests/string/memset_0.c:10: Warning: + dropping duplicate def'n of func chars at tests/string/memset_0.c:10 in favor of that at tests/string/result/memset_0.c:26 +[kernel] tests/string/memset_0.c:15: Warning: + dropping duplicate def'n of func uchars at tests/string/memset_0.c:15 in favor of that at tests/string/result/memset_0.c:50 +[kernel] tests/string/memset_0.c:20: Warning: + dropping duplicate def'n of func nested_chars at tests/string/memset_0.c:20 in favor of that at tests/string/result/memset_0.c:78 +[kernel] tests/string/memset_0.c:25: Warning: + dropping duplicate def'n of func integer at tests/string/memset_0.c:25 in favor of that at tests/string/result/memset_0.c:104 +[kernel] tests/string/memset_0.c:30: Warning: + dropping duplicate def'n of func floats at tests/string/memset_0.c:30 in favor of that at tests/string/result/memset_0.c:130 +[kernel] tests/string/memset_0.c:35: Warning: + dropping duplicate def'n of func with_named at tests/string/memset_0.c:35 in favor of that at tests/string/result/memset_0.c:137 +[kernel] tests/string/memset_0.c:40: Warning: + dropping duplicate def'n of func structure at tests/string/memset_0.c:40 in favor of that at tests/string/result/memset_0.c:164 +[kernel] tests/string/memset_0.c:45: Warning: + dropping duplicate def'n of func pointers at tests/string/memset_0.c:45 in favor of that at tests/string/result/memset_0.c:190 +[kernel] tests/string/memset_0.c:50: Warning: + dropping duplicate def'n of func nested at tests/string/memset_0.c:50 in favor of that at tests/string/result/memset_0.c:218 /* Generated by Frama-C */ #include "stddef.h" #include "string.h" diff --git a/src/plugins/builtin/tests/functions/oracle/memset_FF.res.oracle b/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle similarity index 88% rename from src/plugins/builtin/tests/functions/oracle/memset_FF.res.oracle rename to src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle index 90cc89ab1c79d5a2620c2fa89c07c6f0b6ad586f..bc10dec771d696148a345a43d2a3159531280b45 100644 --- a/src/plugins/builtin/tests/functions/oracle/memset_FF.res.oracle +++ b/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle @@ -1,4 +1,4 @@ -[kernel] Parsing tests/functions/memset_FF.c (with preprocessing) +[kernel] Parsing tests/string/memset_FF.c (with preprocessing) /* Generated by Frama-C */ #include "stddef.h" #include "string.h" @@ -363,36 +363,36 @@ void nested(int (*dest)[10], int n) } -[kernel] Parsing tests/functions/result/memset_FF.c (with preprocessing) -[kernel] Parsing tests/functions/memset_FF.c (with preprocessing) -[kernel] tests/functions/memset_FF.c:10: Warning: - dropping duplicate def'n of func chars at tests/functions/memset_FF.c:10 in favor of that at tests/functions/result/memset_FF.c:26 -[kernel] tests/functions/memset_FF.c:15: Warning: - dropping duplicate def'n of func uchars at tests/functions/memset_FF.c:15 in favor of that at tests/functions/result/memset_FF.c:50 -[kernel] tests/functions/memset_FF.c:20: Warning: - dropping duplicate def'n of func nested_chars at tests/functions/memset_FF.c:20 in favor of that at tests/functions/result/memset_FF.c:79 -[kernel] tests/functions/memset_FF.c:25: Warning: - dropping duplicate def'n of func integer at tests/functions/memset_FF.c:25 in favor of that at tests/functions/result/memset_FF.c:105 -[kernel] tests/functions/memset_FF.c:30: Warning: - dropping duplicate def'n of func unsigned_integer at tests/functions/memset_FF.c:30 in favor of that at tests/functions/result/memset_FF.c:131 -[kernel] tests/functions/memset_FF.c:35: Warning: - dropping duplicate def'n of func long_integer at tests/functions/memset_FF.c:35 in favor of that at tests/functions/result/memset_FF.c:158 -[kernel] tests/functions/memset_FF.c:40: Warning: - dropping duplicate def'n of func unsigned_long_integer at tests/functions/memset_FF.c:40 in favor of that at tests/functions/result/memset_FF.c:184 -[kernel] tests/functions/memset_FF.c:45: Warning: - dropping duplicate def'n of func long_long_integer at tests/functions/memset_FF.c:45 in favor of that at tests/functions/result/memset_FF.c:212 -[kernel] tests/functions/memset_FF.c:50: Warning: - dropping duplicate def'n of func unsigned_long_long_integer at tests/functions/memset_FF.c:50 in favor of that at tests/functions/result/memset_FF.c:240 -[kernel] tests/functions/memset_FF.c:56: Warning: - dropping duplicate def'n of func floats at tests/functions/memset_FF.c:56 in favor of that at tests/functions/result/memset_FF.c:267 -[kernel] tests/functions/memset_FF.c:61: Warning: - dropping duplicate def'n of func with_named at tests/functions/memset_FF.c:61 in favor of that at tests/functions/result/memset_FF.c:274 -[kernel] tests/functions/memset_FF.c:66: Warning: - dropping duplicate def'n of func structure at tests/functions/memset_FF.c:66 in favor of that at tests/functions/result/memset_FF.c:302 -[kernel] tests/functions/memset_FF.c:71: Warning: - dropping duplicate def'n of func pointers at tests/functions/memset_FF.c:71 in favor of that at tests/functions/result/memset_FF.c:328 -[kernel] tests/functions/memset_FF.c:76: Warning: - dropping duplicate def'n of func nested at tests/functions/memset_FF.c:76 in favor of that at tests/functions/result/memset_FF.c:356 +[kernel] Parsing tests/string/result/memset_FF.c (with preprocessing) +[kernel] Parsing tests/string/memset_FF.c (with preprocessing) +[kernel] tests/string/memset_FF.c:10: Warning: + dropping duplicate def'n of func chars at tests/string/memset_FF.c:10 in favor of that at tests/string/result/memset_FF.c:26 +[kernel] tests/string/memset_FF.c:15: Warning: + dropping duplicate def'n of func uchars at tests/string/memset_FF.c:15 in favor of that at tests/string/result/memset_FF.c:50 +[kernel] tests/string/memset_FF.c:20: Warning: + dropping duplicate def'n of func nested_chars at tests/string/memset_FF.c:20 in favor of that at tests/string/result/memset_FF.c:79 +[kernel] tests/string/memset_FF.c:25: Warning: + dropping duplicate def'n of func integer at tests/string/memset_FF.c:25 in favor of that at tests/string/result/memset_FF.c:105 +[kernel] tests/string/memset_FF.c:30: Warning: + dropping duplicate def'n of func unsigned_integer at tests/string/memset_FF.c:30 in favor of that at tests/string/result/memset_FF.c:131 +[kernel] tests/string/memset_FF.c:35: Warning: + dropping duplicate def'n of func long_integer at tests/string/memset_FF.c:35 in favor of that at tests/string/result/memset_FF.c:158 +[kernel] tests/string/memset_FF.c:40: Warning: + dropping duplicate def'n of func unsigned_long_integer at tests/string/memset_FF.c:40 in favor of that at tests/string/result/memset_FF.c:184 +[kernel] tests/string/memset_FF.c:45: Warning: + dropping duplicate def'n of func long_long_integer at tests/string/memset_FF.c:45 in favor of that at tests/string/result/memset_FF.c:212 +[kernel] tests/string/memset_FF.c:50: Warning: + dropping duplicate def'n of func unsigned_long_long_integer at tests/string/memset_FF.c:50 in favor of that at tests/string/result/memset_FF.c:240 +[kernel] tests/string/memset_FF.c:56: Warning: + dropping duplicate def'n of func floats at tests/string/memset_FF.c:56 in favor of that at tests/string/result/memset_FF.c:267 +[kernel] tests/string/memset_FF.c:61: Warning: + dropping duplicate def'n of func with_named at tests/string/memset_FF.c:61 in favor of that at tests/string/result/memset_FF.c:274 +[kernel] tests/string/memset_FF.c:66: Warning: + dropping duplicate def'n of func structure at tests/string/memset_FF.c:66 in favor of that at tests/string/result/memset_FF.c:302 +[kernel] tests/string/memset_FF.c:71: Warning: + dropping duplicate def'n of func pointers at tests/string/memset_FF.c:71 in favor of that at tests/string/result/memset_FF.c:328 +[kernel] tests/string/memset_FF.c:76: Warning: + dropping duplicate def'n of func nested at tests/string/memset_FF.c:76 in favor of that at tests/string/result/memset_FF.c:356 /* Generated by Frama-C */ #include "stddef.h" #include "string.h" diff --git a/src/plugins/builtin/tests/functions/oracle/memset_value.res.oracle b/src/plugins/builtin/tests/string/oracle/memset_value.res.oracle similarity index 72% rename from src/plugins/builtin/tests/functions/oracle/memset_value.res.oracle rename to src/plugins/builtin/tests/string/oracle/memset_value.res.oracle index 3e6db003d1049dfe02b3d2ebc4c79a71c7466461..e63b609e65b9a6d11742be01d5bd5093edf28192 100644 --- a/src/plugins/builtin/tests/functions/oracle/memset_value.res.oracle +++ b/src/plugins/builtin/tests/string/oracle/memset_value.res.oracle @@ -1,24 +1,14 @@ -[kernel] Parsing tests/functions/memset_value.c (with preprocessing) -[builtin] tests/functions/memset_value.c:26: Warning: - Ignore call: not well typed -[builtin] tests/functions/memset_value.c:27: Warning: - Ignore call: not well typed -[builtin] tests/functions/memset_value.c:31: Warning: - Ignore call: not well typed -[builtin] tests/functions/memset_value.c:32: Warning: - Ignore call: not well typed -[builtin] tests/functions/memset_value.c:36: Warning: - Ignore call: not well typed -[builtin] tests/functions/memset_value.c:37: Warning: - Ignore call: not well typed -[builtin] tests/functions/memset_value.c:41: Warning: - Ignore call: not well typed -[builtin] tests/functions/memset_value.c:42: Warning: - Ignore call: not well typed -[builtin] tests/functions/memset_value.c:46: Warning: - Ignore call: not well typed -[builtin] tests/functions/memset_value.c:47: Warning: - Ignore call: not well typed +[kernel] Parsing tests/string/memset_value.c (with preprocessing) +[builtin] tests/string/memset_value.c:26: Warning: Ignore call: not well typed +[builtin] tests/string/memset_value.c:27: Warning: Ignore call: not well typed +[builtin] tests/string/memset_value.c:31: Warning: Ignore call: not well typed +[builtin] tests/string/memset_value.c:32: Warning: Ignore call: not well typed +[builtin] tests/string/memset_value.c:36: Warning: Ignore call: not well typed +[builtin] tests/string/memset_value.c:37: Warning: Ignore call: not well typed +[builtin] tests/string/memset_value.c:41: Warning: Ignore call: not well typed +[builtin] tests/string/memset_value.c:42: Warning: Ignore call: not well typed +[builtin] tests/string/memset_value.c:46: Warning: Ignore call: not well typed +[builtin] tests/string/memset_value.c:47: Warning: Ignore call: not well typed /* Generated by Frama-C */ #include "stddef.h" #include "string.h" @@ -141,24 +131,24 @@ void nested(int (*dest)[10], int n, int value) } -[kernel] Parsing tests/functions/result/memset_value.c (with preprocessing) -[kernel] Parsing tests/functions/memset_value.c (with preprocessing) -[kernel] tests/functions/memset_value.c:10: Warning: - dropping duplicate def'n of func chars at tests/functions/memset_value.c:10 in favor of that at tests/functions/result/memset_value.c:26 -[kernel] tests/functions/memset_value.c:15: Warning: - dropping duplicate def'n of func uchars at tests/functions/memset_value.c:15 in favor of that at tests/functions/result/memset_value.c:50 -[kernel] tests/functions/memset_value.c:20: Warning: - dropping duplicate def'n of func nested_chars at tests/functions/memset_value.c:20 in favor of that at tests/functions/result/memset_value.c:78 -[kernel] tests/functions/memset_value.c:25: Warning: - dropping duplicate def'n of func integer at tests/functions/memset_value.c:25 in favor of that at tests/functions/result/memset_value.c:85 -[kernel] tests/functions/memset_value.c:30: Warning: - dropping duplicate def'n of func with_named at tests/functions/memset_value.c:30 in favor of that at tests/functions/result/memset_value.c:92 -[kernel] tests/functions/memset_value.c:35: Warning: - dropping duplicate def'n of func structure at tests/functions/memset_value.c:35 in favor of that at tests/functions/result/memset_value.c:99 -[kernel] tests/functions/memset_value.c:40: Warning: - dropping duplicate def'n of func pointers at tests/functions/memset_value.c:40 in favor of that at tests/functions/result/memset_value.c:107 -[kernel] tests/functions/memset_value.c:45: Warning: - dropping duplicate def'n of func nested at tests/functions/memset_value.c:45 in favor of that at tests/functions/result/memset_value.c:114 +[kernel] Parsing tests/string/result/memset_value.c (with preprocessing) +[kernel] Parsing tests/string/memset_value.c (with preprocessing) +[kernel] tests/string/memset_value.c:10: Warning: + dropping duplicate def'n of func chars at tests/string/memset_value.c:10 in favor of that at tests/string/result/memset_value.c:26 +[kernel] tests/string/memset_value.c:15: Warning: + dropping duplicate def'n of func uchars at tests/string/memset_value.c:15 in favor of that at tests/string/result/memset_value.c:50 +[kernel] tests/string/memset_value.c:20: Warning: + dropping duplicate def'n of func nested_chars at tests/string/memset_value.c:20 in favor of that at tests/string/result/memset_value.c:78 +[kernel] tests/string/memset_value.c:25: Warning: + dropping duplicate def'n of func integer at tests/string/memset_value.c:25 in favor of that at tests/string/result/memset_value.c:85 +[kernel] tests/string/memset_value.c:30: Warning: + dropping duplicate def'n of func with_named at tests/string/memset_value.c:30 in favor of that at tests/string/result/memset_value.c:92 +[kernel] tests/string/memset_value.c:35: Warning: + dropping duplicate def'n of func structure at tests/string/memset_value.c:35 in favor of that at tests/string/result/memset_value.c:99 +[kernel] tests/string/memset_value.c:40: Warning: + dropping duplicate def'n of func pointers at tests/string/memset_value.c:40 in favor of that at tests/string/result/memset_value.c:107 +[kernel] tests/string/memset_value.c:45: Warning: + dropping duplicate def'n of func nested at tests/string/memset_value.c:45 in favor of that at tests/string/result/memset_value.c:114 /* Generated by Frama-C */ #include "stddef.h" #include "string.h" diff --git a/src/plugins/builtin/tests/functions/test_config b/src/plugins/builtin/tests/string/test_config similarity index 100% rename from src/plugins/builtin/tests/functions/test_config rename to src/plugins/builtin/tests/string/test_config