Skip to content

Commit a618231

Browse files
committed
C library/getenv test: actually try to dereference the result
Our regression test would previously succeed even when no implementation of `getenv` was provided.
1 parent 9a3a142 commit a618231

File tree

2 files changed

+5
-1
lines changed

2 files changed

+5
-1
lines changed

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,4 +5,8 @@ int main()
55
char *something;
66
// there should not be any overflow in there
77
something = getenv("HOME");
8+
if(something != NULL)
9+
return something[0];
10+
else
11+
return 0;
812
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --pointer-check --bounds-check
3+
--signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --pointer-check --bounds-check --memory-leak-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

0 commit comments

Comments
 (0)