From 8eeb5fa7bb5972787ba6866eb81aa6d5c6c03b0b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Jul 2025 07:17:53 +0000 Subject: [PATCH 1/2] Implement all *scanf regression tests We already had working tests for scanf and fscanf, and can easily extend this to all variants. --- regression/cbmc-library/sscanf-01/main.c | 5 +++-- regression/cbmc-library/sscanf-01/test.desc | 10 ++++++---- regression/cbmc-library/vfscanf-01/main.c | 15 +++++++++++++-- regression/cbmc-library/vfscanf-01/test.desc | 10 ++++++---- regression/cbmc-library/vscanf-01/main.c | 15 +++++++++++++-- regression/cbmc-library/vscanf-01/test.desc | 10 ++++++---- regression/cbmc-library/vsscanf-01/main.c | 15 +++++++++++++-- regression/cbmc-library/vsscanf-01/test.desc | 10 ++++++---- 8 files changed, 66 insertions(+), 24 deletions(-) diff --git a/regression/cbmc-library/sscanf-01/main.c b/regression/cbmc-library/sscanf-01/main.c index 39a5b02142f..4dc316ec9a9 100644 --- a/regression/cbmc-library/sscanf-01/main.c +++ b/regression/cbmc-library/sscanf-01/main.c @@ -3,7 +3,8 @@ int main() { - sscanf(); - assert(0); + char dest[10]; + int result = sscanf("hello", "%s", dest); + assert(result == 1); return 0; } diff --git a/regression/cbmc-library/sscanf-01/test.desc b/regression/cbmc-library/sscanf-01/test.desc index 9542d988e8d..bd3c75dc6e0 100644 --- a/regression/cbmc-library/sscanf-01/test.desc +++ b/regression/cbmc-library/sscanf-01/test.desc @@ -1,8 +1,10 @@ -KNOWNBUG +CORE main.c ---pointer-check --bounds-check -^EXIT=0$ + +^\[main.assertion.1\] line 8 assertion result == 1: FAILURE$ +^\*\* 1 of \d+ failed +^VERIFICATION FAILED$ +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring diff --git a/regression/cbmc-library/vfscanf-01/main.c b/regression/cbmc-library/vfscanf-01/main.c index 9152d465a87..362838521f9 100644 --- a/regression/cbmc-library/vfscanf-01/main.c +++ b/regression/cbmc-library/vfscanf-01/main.c @@ -1,9 +1,20 @@ #include +#include #include +int xscanf(const char *format, ...) +{ + va_list list; + va_start(list, format); + int result = vfscanf(stdin, format, list); + va_end(list); + return result; +} + int main() { - vfscanf(); - assert(0); + char dest[10]; + int result = xscanf("%s", dest); + assert(result == 1); return 0; } diff --git a/regression/cbmc-library/vfscanf-01/test.desc b/regression/cbmc-library/vfscanf-01/test.desc index 9542d988e8d..7d421da2cc5 100644 --- a/regression/cbmc-library/vfscanf-01/test.desc +++ b/regression/cbmc-library/vfscanf-01/test.desc @@ -1,8 +1,10 @@ -KNOWNBUG +CORE main.c ---pointer-check --bounds-check -^EXIT=0$ + +^\[main.assertion.1\] line 18 assertion result == 1: FAILURE$ +^\*\* 1 of \d+ failed +^VERIFICATION FAILED$ +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring diff --git a/regression/cbmc-library/vscanf-01/main.c b/regression/cbmc-library/vscanf-01/main.c index 0bee36a6daa..1c71b18e5f8 100644 --- a/regression/cbmc-library/vscanf-01/main.c +++ b/regression/cbmc-library/vscanf-01/main.c @@ -1,9 +1,20 @@ #include +#include #include +int xscanf(const char *format, ...) +{ + va_list list; + va_start(list, format); + int result = vscanf(format, list); + va_end(list); + return result; +} + int main() { - vscanf(); - assert(0); + char dest[10]; + int result = xscanf("%s", dest); + assert(result == 1); return 0; } diff --git a/regression/cbmc-library/vscanf-01/test.desc b/regression/cbmc-library/vscanf-01/test.desc index 9542d988e8d..7d421da2cc5 100644 --- a/regression/cbmc-library/vscanf-01/test.desc +++ b/regression/cbmc-library/vscanf-01/test.desc @@ -1,8 +1,10 @@ -KNOWNBUG +CORE main.c ---pointer-check --bounds-check -^EXIT=0$ + +^\[main.assertion.1\] line 18 assertion result == 1: FAILURE$ +^\*\* 1 of \d+ failed +^VERIFICATION FAILED$ +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring diff --git a/regression/cbmc-library/vsscanf-01/main.c b/regression/cbmc-library/vsscanf-01/main.c index 672eaddb2f8..016f0a9f0a9 100644 --- a/regression/cbmc-library/vsscanf-01/main.c +++ b/regression/cbmc-library/vsscanf-01/main.c @@ -1,9 +1,20 @@ #include +#include #include +int xscanf(const char *format, ...) +{ + va_list list; + va_start(list, format); + int result = vsscanf("hello", format, list); + va_end(list); + return result; +} + int main() { - vsscanf(); - assert(0); + char dest[10]; + int result = xscanf("%s", dest); + assert(result == 1); return 0; } diff --git a/regression/cbmc-library/vsscanf-01/test.desc b/regression/cbmc-library/vsscanf-01/test.desc index 9542d988e8d..7d421da2cc5 100644 --- a/regression/cbmc-library/vsscanf-01/test.desc +++ b/regression/cbmc-library/vsscanf-01/test.desc @@ -1,8 +1,10 @@ -KNOWNBUG +CORE main.c ---pointer-check --bounds-check -^EXIT=0$ + +^\[main.assertion.1\] line 18 assertion result == 1: FAILURE$ +^\*\* 1 of \d+ failed +^VERIFICATION FAILED$ +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring From f6fd739c727f76763a4418695ae736056135044d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 9 Mar 2023 12:03:21 +0000 Subject: [PATCH 2/2] C front-end: tolerate type differences with asm renaming The example found in glibc shows how asm renaming may be combined with changes in return type names (even when there isn't actually a bit-level difference amongst the types). Weakening the asm-renamed declaration by marking it "incomplete" works around this problem. --- regression/ansi-c/asm4/main.c | 26 ++++++++++++++++++++++++++ regression/ansi-c/asm4/test.desc | 8 ++++++++ src/ansi-c/c_typecheck_base.cpp | 4 ++++ 3 files changed, 38 insertions(+) create mode 100644 regression/ansi-c/asm4/main.c create mode 100644 regression/ansi-c/asm4/test.desc diff --git a/regression/ansi-c/asm4/main.c b/regression/ansi-c/asm4/main.c new file mode 100644 index 00000000000..a22fd92ddc7 --- /dev/null +++ b/regression/ansi-c/asm4/main.c @@ -0,0 +1,26 @@ +// from Fedora's glibc +struct dirent +{ + int dummy; +}; + +struct dirent64 +{ + int dummy; +}; + +#ifdef __GNUC__ +extern struct dirent *readdir(void *__dirp) __asm__( + "" + "readdir64"); +extern struct dirent64 *readdir64(void *__dirp); +#endif + +int main() +{ +#ifdef __GNUC__ + int x; + (void)readdir(&x); +#endif + return 0; +} diff --git a/regression/ansi-c/asm4/test.desc b/regression/ansi-c/asm4/test.desc new file mode 100644 index 00000000000..b9903aa3c3d --- /dev/null +++ b/regression/ansi-c/asm4/test.desc @@ -0,0 +1,8 @@ +CORE test-c++-front-end +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index f11e08f7e14..f0c012b29fa 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -668,6 +668,10 @@ void c_typecheck_baset::apply_asm_label( { symbol.name=asm_label; symbol.base_name=asm_label; + // asm renaming may be combined with varied return types - make sure the + // actual definition sets the final type + if(symbol.type.id() == ID_code) + symbol.type.set(ID_C_incomplete, true); } if(symbol.name!=orig_name)