Skip to content

Commit eb763ff

Browse files
committed
C library: make sleep() branch free
The if(...) assignment can be replaced by an assume statement, which avoids a branch. Also, enable the regression test of the sleep function.
1 parent 55d32b5 commit eb763ff

File tree

3 files changed

+3
-5
lines changed

3 files changed

+3
-5
lines changed

regression/cbmc-library/sleep-01/main.c

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@
33

44
int main()
55
{
6-
sleep();
7-
assert(0);
6+
assert(sleep(42) <= 42);
87
return 0;
98
}

regression/cbmc-library/sleep-01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

src/ansi-c/library/unistd.c

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,7 @@ unsigned int sleep(unsigned int seconds)
77
__CPROVER_HIDE:;
88
// do nothing, but return nondet value
99
unsigned remaining_time=__VERIFIER_nondet_unsigned();
10-
11-
if(remaining_time>seconds) remaining_time=seconds;
10+
__CPROVER_assume(remaining_time <= seconds);
1211

1312
return remaining_time;
1413
}

0 commit comments

Comments
 (0)