From d77d6c6648a1aaf8cafefd1458500c71e2c271ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Oct 2014 13:24:31 -0700 Subject: [PATCH] update parameter checking for doubles, and fix error reporting Signed-off-by: Nikolaj Bjorner --- src/util/gparams.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 6397ad377..83157a0b0 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -233,22 +233,22 @@ public: void validate_type(symbol const& name, char const* value, param_descrs const& d) { param_kind k = d.get_kind(name); std::stringstream strm; - + char const* _value = value; switch (k) { case CPK_UINT: for (; *value; ++value) { if (!('0' <= *value && *value <= '9')) { strm << "Expected values for parameter " << name - << " is an unsigned integer. It was given argument '" << value << "'"; + << " is an unsigned integer. It was given argument '" << _value << "'"; throw default_exception(strm.str()); } } break; case CPK_DOUBLE: for (; *value; ++value) { - if (!('0' <= *value && *value <= '9') && *value != '.' && *value != '-') { + if (!('0' <= *value && *value <= '9') && *value != '.' && *value != '-' && *value != '/') { strm << "Expected values for parameter " << name - << " is a double. It was given argument '" << value << "'"; + << " is a double. It was given argument '" << _value << "'"; throw default_exception(strm.str()); } }