Skip to content

Commit ecfc918

Browse files
committed
Avoid conversion check failure sysconf library model
`errno` is signed. Also, fix test patterns and spelling mistakes in comments.
1 parent 63b8b71 commit ecfc918

File tree

2 files changed

+8
-8
lines changed

2 files changed

+8
-8
lines changed
Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
CORE unix
22
main.c
3-
3+
--pointer-check --bounds-check --conversion-check
44
^\[main.assertion.\d+\] line \d+ ARG\_MAX is not supported: FAILURE$
55
^\[main.assertion.\d+\] line \d+ sysconf\(\) error: FAILURE$
66
^\[main.assertion.\d+\] line \d+ ARG\_MAX is supported: FAILURE$
7-
^\*\* 3 of 3 failed .*$
7+
^\*\* 3 of \d+ failed .*$
88
^VERIFICATION FAILED$
99
^EXIT=10$
1010
^SIGNAL=0$
1111
--
12-
^WARNING: no body for function sysconf
12+
^\*\*\*\* WARNING: no body for function sysconf

src/ansi-c/library/unistd.c

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -328,7 +328,7 @@ ret_type _read(int fildes, void *buf, size_type nbyte)
328328
#endif
329329

330330
long __VERIFIER_nondet_long(void);
331-
unsigned int __VERIFIER_nondet_unsigned_int(void);
331+
int __VERIFIER_nondet_int(void);
332332

333333
long sysconf(int name);
334334

@@ -340,13 +340,13 @@ __CPROVER_HIDE:;
340340
(void)name;
341341
long retval = __VERIFIER_nondet_long();
342342

343-
// We should keep errno as non-determinist as possible, since this model
344-
// nver takes into account the name input.
345-
errno = __VERIFIER_nondet_unsigned_int();
343+
// We should keep errno as non-deterministic as possible, since this model
344+
// never takes into account the name input.
345+
errno = __VERIFIER_nondet_int();
346346

347347
// Spec states "some returned values may be huge; they are not suitable
348348
// for allocating memory". There aren't also guarantees about return
349-
// values being strickly equal or greater to -1.
349+
// values being strictly equal or greater to -1.
350350
// Thus, modelling it as non-deterministic.
351351
return retval;
352352
}

0 commit comments

Comments
 (0)