From ecfc91892796c5410743638816e0080f0bed489e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 24 Jul 2023 08:47:24 +0000 Subject: [PATCH] Avoid conversion check failure sysconf library model `errno` is signed. Also, fix test patterns and spelling mistakes in comments. --- regression/cbmc-library/sysconf-01/test.desc | 6 +++--- src/ansi-c/library/unistd.c | 10 +++++----- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/regression/cbmc-library/sysconf-01/test.desc b/regression/cbmc-library/sysconf-01/test.desc index 49ed341331a..cd6a6e76616 100644 --- a/regression/cbmc-library/sysconf-01/test.desc +++ b/regression/cbmc-library/sysconf-01/test.desc @@ -1,12 +1,12 @@ CORE unix main.c - +--pointer-check --bounds-check --conversion-check ^\[main.assertion.\d+\] line \d+ ARG\_MAX is not supported: FAILURE$ ^\[main.assertion.\d+\] line \d+ sysconf\(\) error: FAILURE$ ^\[main.assertion.\d+\] line \d+ ARG\_MAX is supported: FAILURE$ -^\*\* 3 of 3 failed .*$ +^\*\* 3 of \d+ failed .*$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ -- -^WARNING: no body for function sysconf +^\*\*\*\* WARNING: no body for function sysconf diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c index dc2983ba748..b2daf2dee07 100644 --- a/src/ansi-c/library/unistd.c +++ b/src/ansi-c/library/unistd.c @@ -328,7 +328,7 @@ ret_type _read(int fildes, void *buf, size_type nbyte) #endif long __VERIFIER_nondet_long(void); -unsigned int __VERIFIER_nondet_unsigned_int(void); +int __VERIFIER_nondet_int(void); long sysconf(int name); @@ -340,13 +340,13 @@ __CPROVER_HIDE:; (void)name; long retval = __VERIFIER_nondet_long(); - // We should keep errno as non-determinist as possible, since this model - // nver takes into account the name input. - errno = __VERIFIER_nondet_unsigned_int(); + // We should keep errno as non-deterministic as possible, since this model + // never takes into account the name input. + errno = __VERIFIER_nondet_int(); // Spec states "some returned values may be huge; they are not suitable // for allocating memory". There aren't also guarantees about return - // values being strickly equal or greater to -1. + // values being strictly equal or greater to -1. // Thus, modelling it as non-deterministic. return retval; }