1 files changed, 9 insertions, 0 deletions
diff --git a/include/klee/Internal/System/Time.h b/include/klee/Internal/System/Time.h
index 5229c8c9..14d23536 100644
--- a/include/klee/Internal/System/Time.h
+++ b/include/klee/Internal/System/Time.h
@@ -10,10 +10,19 @@
 #ifndef KLEE_UTIL_TIME_H
 #define KLEE_UTIL_TIME_H
 
+#include <llvm/Support/TimeValue.h>
+
 namespace klee {
   namespace util {
+
+    /// Seconds spent by this process in user mode.
     double getUserTime();
+
+    /// Wall time in seconds.
     double getWallTime();
+
+    /// Wall time as TimeValue object.
+    llvm::sys::TimeValue getWallTimeVal();
   }
 }