From 4eab1f5057a923d2a0d1075ff83b8ed32aac7ffd Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 21 Oct 2019 15:49:43 +0200
Subject: [PATCH] [Libc] fix libc spec: utimes; add test
---
share/libc/sys/time.h | 5 +-
tests/libc/oracle/sys_time.res.oracle | 62 ------------------
tests/libc/oracle/sys_time_h.res.oracle | 83 +++++++++++++++++++++++++
tests/libc/{sys_time.c => sys_time_h.c} | 9 +++
4 files changed, 95 insertions(+), 64 deletions(-)
delete mode 100644 tests/libc/oracle/sys_time.res.oracle
create mode 100644 tests/libc/oracle/sys_time_h.res.oracle
rename tests/libc/{sys_time.c => sys_time_h.c} (74%)
diff --git a/share/libc/sys/time.h b/share/libc/sys/time.h
index 15213f4cbb1..afeb1fb4af0 100644
--- a/share/libc/sys/time.h
+++ b/share/libc/sys/time.h
@@ -47,8 +47,9 @@ struct timezone {
/*@
requires valid_path: valid_read_string(path);
- requires valid_times: \valid_read(times+(0..1));
- assigns \result \from indirect:path[0..strlen(path)], indirect:times[0..1];
+ requires valid_times_or_null: \valid_read(times+(0..1)) || times == \null;
+ assigns \result \from indirect:path[0..strlen(path)],
+ indirect:times, indirect:times[0..1];
*/
extern int utimes(const char *path, const struct timeval times[2]);
diff --git a/tests/libc/oracle/sys_time.res.oracle b/tests/libc/oracle/sys_time.res.oracle
deleted file mode 100644
index 18c18fa9f8c..00000000000
--- a/tests/libc/oracle/sys_time.res.oracle
+++ /dev/null
@@ -1,62 +0,0 @@
-[kernel] Parsing tests/libc/sys_time.c (with preprocessing)
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
-
-[eva] computing for function setitimer <- main.
- Called from tests/libc/sys_time.c:6.
-[eva] using specification for function setitimer
-[eva] tests/libc/sys_time.c:6:
- function setitimer: precondition 'valid_new_value' got status valid.
-[eva] tests/libc/sys_time.c:6:
- function setitimer: precondition 'old_value_null_or_valid' got status valid.
-[eva:invalid-assigns] tests/libc/sys_time.c:6:
- Completely invalid destination for assigns clause *old_value. Ignoring.
-[eva] Done for function setitimer
-[eva] tests/libc/sys_time.c:7: assertion got status valid.
-[eva] computing for function setitimer <- main.
- Called from tests/libc/sys_time.c:9.
-[eva] tests/libc/sys_time.c:9:
- function setitimer: precondition 'valid_new_value' got status valid.
-[eva] tests/libc/sys_time.c:9:
- function setitimer: precondition 'old_value_null_or_valid' got status valid.
-[eva] Done for function setitimer
-[eva] tests/libc/sys_time.c:10: assertion got status valid.
-[eva] tests/libc/sys_time.c:11: assertion got status valid.
-[eva] computing for function getitimer <- main.
- Called from tests/libc/sys_time.c:12.
-[eva] using specification for function getitimer
-[eva] tests/libc/sys_time.c:12:
- function getitimer: precondition 'valid_curr_value' got status valid.
-[eva] Done for function getitimer
-[eva] tests/libc/sys_time.c:13: assertion got status valid.
-[eva] tests/libc/sys_time.c:14: assertion got status valid.
-[eva] computing for function getitimer <- main.
- Called from tests/libc/sys_time.c:16.
-[eva] tests/libc/sys_time.c:16:
- function getitimer: precondition 'valid_curr_value' got status valid.
-[eva] Done for function getitimer
-[eva] tests/libc/sys_time.c:17: assertion got status valid.
-[eva] computing for function setitimer <- main.
- Called from tests/libc/sys_time.c:19.
-[eva] tests/libc/sys_time.c:19:
- function setitimer: precondition 'valid_new_value' got status valid.
-[eva] tests/libc/sys_time.c:19:
- function setitimer: precondition 'old_value_null_or_valid' got status valid.
-[eva] Done for function setitimer
-[eva] tests/libc/sys_time.c:20: assertion got status valid.
-[eva] Recording results for main
-[eva] done for function main
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main:
- i1.it_interval.tv_sec ∈ {1}
- .it_interval.tv_usec ∈ {100}
- .it_value.tv_sec ∈ {2}
- .it_value.tv_usec ∈ {200}
- res ∈ {-1}
- i2.it_interval.tv_sec ∈ [--..--]
- .it_interval.tv_usec ∈ {1000000}
- .it_value ∈ [--..--]
- INVALID_ITIMER ∈ {-1}
- __retres ∈ {0}
diff --git a/tests/libc/oracle/sys_time_h.res.oracle b/tests/libc/oracle/sys_time_h.res.oracle
new file mode 100644
index 00000000000..56221db7dec
--- /dev/null
+++ b/tests/libc/oracle/sys_time_h.res.oracle
@@ -0,0 +1,83 @@
+[kernel] Parsing tests/libc/sys_time_h.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] computing for function setitimer <- main.
+ Called from tests/libc/sys_time_h.c:6.
+[eva] using specification for function setitimer
+[eva] tests/libc/sys_time_h.c:6:
+ function setitimer: precondition 'valid_new_value' got status valid.
+[eva] tests/libc/sys_time_h.c:6:
+ function setitimer: precondition 'old_value_null_or_valid' got status valid.
+[eva:invalid-assigns] tests/libc/sys_time_h.c:6:
+ Completely invalid destination for assigns clause *old_value. Ignoring.
+[eva] Done for function setitimer
+[eva] tests/libc/sys_time_h.c:7: assertion got status valid.
+[eva] computing for function setitimer <- main.
+ Called from tests/libc/sys_time_h.c:9.
+[eva] tests/libc/sys_time_h.c:9:
+ function setitimer: precondition 'valid_new_value' got status valid.
+[eva] tests/libc/sys_time_h.c:9:
+ function setitimer: precondition 'old_value_null_or_valid' got status valid.
+[eva] Done for function setitimer
+[eva] tests/libc/sys_time_h.c:10: assertion got status valid.
+[eva] tests/libc/sys_time_h.c:11: assertion got status valid.
+[eva] computing for function getitimer <- main.
+ Called from tests/libc/sys_time_h.c:12.
+[eva] using specification for function getitimer
+[eva] tests/libc/sys_time_h.c:12:
+ function getitimer: precondition 'valid_curr_value' got status valid.
+[eva] Done for function getitimer
+[eva] tests/libc/sys_time_h.c:13: assertion got status valid.
+[eva] tests/libc/sys_time_h.c:14: assertion got status valid.
+[eva] computing for function getitimer <- main.
+ Called from tests/libc/sys_time_h.c:16.
+[eva] tests/libc/sys_time_h.c:16:
+ function getitimer: precondition 'valid_curr_value' got status valid.
+[eva] Done for function getitimer
+[eva] tests/libc/sys_time_h.c:17: assertion got status valid.
+[eva] computing for function setitimer <- main.
+ Called from tests/libc/sys_time_h.c:19.
+[eva] tests/libc/sys_time_h.c:19:
+ function setitimer: precondition 'valid_new_value' got status valid.
+[eva] tests/libc/sys_time_h.c:19:
+ function setitimer: precondition 'old_value_null_or_valid' got status valid.
+[eva] Done for function setitimer
+[eva] tests/libc/sys_time_h.c:20: assertion got status valid.
+[eva] computing for function utimes <- main.
+ Called from tests/libc/sys_time_h.c:22.
+[eva] using specification for function utimes
+[eva] tests/libc/sys_time_h.c:22:
+ function utimes: precondition 'valid_path' got status valid.
+[eva] tests/libc/sys_time_h.c:22:
+ function utimes: precondition 'valid_times_or_null' got status valid.
+[eva] Done for function utimes
+[eva] computing for function utimes <- main.
+ Called from tests/libc/sys_time_h.c:28.
+[eva] tests/libc/sys_time_h.c:28:
+ function utimes: precondition 'valid_path' got status valid.
+[eva] tests/libc/sys_time_h.c:28:
+ function utimes: precondition 'valid_times_or_null' got status valid.
+[eva] Done for function utimes
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ i1.it_interval.tv_sec ∈ {1}
+ .it_interval.tv_usec ∈ {100}
+ .it_value.tv_sec ∈ {2}
+ .it_value.tv_usec ∈ {200}
+ res ∈ {-1}
+ i2.it_interval.tv_sec ∈ [--..--]
+ .it_interval.tv_usec ∈ {1000000}
+ .it_value ∈ [--..--]
+ INVALID_ITIMER ∈ {-1}
+ r1 ∈ [--..--]
+ tv[0].tv_sec ∈ {10000000}
+ [0].tv_usec ∈ {999999}
+ [1].tv_sec ∈ {-9000000}
+ [1].tv_usec ∈ {1}
+ r2 ∈ [--..--]
+ __retres ∈ {0}
diff --git a/tests/libc/sys_time.c b/tests/libc/sys_time_h.c
similarity index 74%
rename from tests/libc/sys_time.c
rename to tests/libc/sys_time_h.c
index 51808be3064..2ec5bcf485a 100644
--- a/tests/libc/sys_time.c
+++ b/tests/libc/sys_time_h.c
@@ -18,5 +18,14 @@ int main() {
i2.it_interval.tv_usec = 1000000; // invalid tv_usec
res = setitimer(ITIMER_VIRTUAL, &i2, &i1);
//@ assert res == -1;
+
+ int r1 = utimes("/tmp/utimes", 0);
+ struct timeval tv[2] =
+ {
+ { .tv_sec = 10000000, .tv_usec = 999999 },
+ { .tv_sec = -9000000, .tv_usec = 1 },
+ };
+ int r2 = utimes("/tmp/utimes", tv);
+
return 0;
}
--
GitLab