time: add double type for span multiplications

4 files changed, 17 insertions, 7 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 95bddf8c..488ffa34 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -889,7 +889,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
 
   time::Span timeout = coreSolverTimeout;
   if (isSeeding)
-    timeout *= it->second.size();
+    timeout *= static_cast<unsigned>(it->second.size());
   solver->setTimeout(timeout);
   bool success = solver->evaluate(current, condition, res);
   solver->setTimeout(time::Span());
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
index de24d75d..9d2e8868 100644
--- a/lib/Core/ExecutorTimers.cpp
+++ b/lib/Core/ExecutorTimers.cpp
@@ -169,7 +169,7 @@ void Executor::processTimers(ExecutionState *current,
     if (maxInstTime && current &&
         std::find(removedStates.begin(), removedStates.end(), current) ==
             removedStates.end()) {
-      if (timerTicks*kMilliSecondsPerTick > maxInstTime) {
+      if (timerTicks * kMilliSecondsPerTick > maxInstTime) {
         klee_warning("max-instruction-time exceeded: %.2fs", (timerTicks * kMilliSecondsPerTick).toSeconds());
         terminateStateEarly(*current, "max-instruction-time exceeded");
       }
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index cce83d23..db295468 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -432,7 +432,7 @@ void IterativeDeepeningTimeSearcher::update(
   }
 
   if (baseSearcher->empty()) {
-    time *= 2;
+    time *= 2U;
     klee_message("increased time budget to %f\n", time.toSeconds());
     std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end());
     baseSearcher->update(0, ps, std::vector<ExecutionState *>());
diff --git a/lib/Support/Time.cpp b/lib/Support/Time.cpp
index 7cd9659b..219b07b0 100644
--- a/lib/Support/Time.cpp
+++ b/lib/Support/Time.cpp
@@ -106,13 +106,23 @@ error:
 time::Span& time::Span::operator=(const time::Duration &d) { duration = d; return *this; };
 time::Span& time::Span::operator+=(const time::Span &other) { duration += other.duration; return *this; }
 time::Span& time::Span::operator-=(const time::Span &other) { duration -= other.duration; return *this; }
-time::Span& time::Span::operator*=(const time::Duration::rep &rep) { duration *= rep; return *this; }
+time::Span& time::Span::operator*=(unsigned factor) { duration *= factor; return *this; }
+time::Span& time::Span::operator*=(double factor) {
+  duration = std::chrono::microseconds((std::uint64_t)((double)toMicroseconds() * factor));
+  return *this;
+}
 
 time::Span time::operator+(const time::Span &lhs, const time::Span &rhs) { return time::Span(lhs.duration + rhs.duration); }
 time::Span time::operator-(const time::Span &lhs, const time::Span &rhs) { return time::Span(lhs.duration - rhs.duration); }
-time::Span time::operator*(const time::Span &span, const time::Duration::rep &rep) { return time::Span(span.duration * rep); }
-time::Span time::operator*(const time::Duration::rep &rep, const time::Span &span) { return time::Span(span.duration * rep); }
-time::Span time::operator/(const time::Span &span, const time::Duration::rep &rep) { return time::Span(span.duration / rep); }
+time::Span time::operator*(const time::Span &span, double factor) {
+  return time::Span(std::chrono::microseconds((std::uint64_t)((double)span.toMicroseconds() * factor)));
+};
+time::Span time::operator*(double factor, const time::Span &span) {
+  return time::Span(std::chrono::microseconds((std::uint64_t)((double)span.toMicroseconds() * factor)));
+};
+time::Span time::operator*(const time::Span &span, unsigned factor) { return time::Span(span.duration * factor); }
+time::Span time::operator*(unsigned factor, const time::Span &span) { return time::Span(span.duration * factor); }
+time::Span time::operator/(const time::Span &span, unsigned divisor) { return time::Span(span.duration / divisor); }
 bool time::operator==(const time::Span &lhs, const time::Span &rhs) { return lhs.duration == rhs.duration; }
 bool time::operator<=(const time::Span &lhs, const time::Span &rhs) { return lhs.duration <= rhs.duration; }
 bool time::operator>=(const time::Span &lhs, const time::Span &rhs) { return lhs.duration >= rhs.duration; }