From 7b72db5f4fa2effa329fa23fe2e0193d7b72a5ce Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 17 Feb 2019 09:20:52 +0000 Subject: [PATCH] added test for undeclared functions Follow up from #4211. The type of function symbols must get fixed once the function signature is known. --- regression/ansi-c/undeclared_function/fileA.c | 7 +++++++ regression/ansi-c/undeclared_function/fileB.c | 6 ++++++ .../ansi-c/undeclared_function/undeclared_function1.desc | 8 ++++++++ 3 files changed, 21 insertions(+) create mode 100644 regression/ansi-c/undeclared_function/fileA.c create mode 100644 regression/ansi-c/undeclared_function/fileB.c create mode 100644 regression/ansi-c/undeclared_function/undeclared_function1.desc diff --git a/regression/ansi-c/undeclared_function/fileA.c b/regression/ansi-c/undeclared_function/fileA.c new file mode 100644 index 0000000000..e6f88a9f66 --- /dev/null +++ b/regression/ansi-c/undeclared_function/fileA.c @@ -0,0 +1,7 @@ +// There is no #include here, deliberately, +// to trigger automatic generation of a signature below. + +int main(void) +{ + malloc(4); +} diff --git a/regression/ansi-c/undeclared_function/fileB.c b/regression/ansi-c/undeclared_function/fileB.c new file mode 100644 index 0000000000..08bdda4911 --- /dev/null +++ b/regression/ansi-c/undeclared_function/fileB.c @@ -0,0 +1,6 @@ +#include + +int f() +{ + malloc(4); +} diff --git a/regression/ansi-c/undeclared_function/undeclared_function1.desc b/regression/ansi-c/undeclared_function/undeclared_function1.desc new file mode 100644 index 0000000000..d002ebcf53 --- /dev/null +++ b/regression/ansi-c/undeclared_function/undeclared_function1.desc @@ -0,0 +1,8 @@ +KNOWNBUG +fileA.c +fileB.c --validate-goto-model +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$