mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Added checks for uint parameter values in context_params

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-11-14 17:25:18 +00:00
parent 05eb78ccac
commit 6b5e49c4a1
2 changed files with 29 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/cmd_context/context_params.cpp
View file

@ -48,7 +48,26 @@ void context_params::set_bool(bool & opt, char const * param, char const * value
} }
else { else {
std::stringstream strm; std::stringstream strm;
strm << "invalid value '" << value << "' for Boolean parameter '" << param; strm << "invalid value '" << value << "' for Boolean parameter '" << param << "'";
throw default_exception(strm.str());
}
}
void context_params::set_uint(unsigned & opt, char const * param, char const * value) {
bool is_uint = true;
size_t sz = strlen(value);
for (unsigned i = 0; i < sz; i++) {
if (!(value[i] >= '0' && value[i] <= '9'))
is_uint = false;
}
if (is_uint) {
long val = strtol(value, 0, 10);
opt = static_cast<unsigned>(val);
}
else {
std::stringstream strm;
strm << "invalid value '" << value << "' for unsigned int parameter '" << param << "'";
throw default_exception(strm.str()); throw default_exception(strm.str());
} }
} }
@ -63,12 +82,10 @@ void context_params::set(char const * param, char const * value) {
p[i] = '_'; p[i] = '_';
} }
if (p == "timeout") { if (p == "timeout") {
long val = strtol(value, 0, 10); set_uint(m_timeout, param, value);
m_timeout = static_cast<unsigned>(val);
} }
else if (p == "rlimit") { else if (p == "rlimit") {
long val = strtol(value, 0, 10); set_uint(m_rlimit, param, value);
m_rlimit = static_cast<unsigned>(val);
} }
else if (p == "type_check" || p == "well_sorted_check") { else if (p == "type_check" || p == "well_sorted_check") {
set_bool(m_well_sorted_check, param, value); set_bool(m_well_sorted_check, param, value);
@ -110,7 +127,7 @@ void context_params::set(char const * param, char const * value) {
strm << "unknown parameter '" << p << "'\n"; strm << "unknown parameter '" << p << "'\n";
strm << "Legal parameters are:\n"; strm << "Legal parameters are:\n";
d.display(strm, 2, false, false); d.display(strm, 2, false, false);
throw default_exception(strm.str()); throw default_exception(strm.str());
} }
} }
@ -174,8 +191,8 @@ void context_params::get_solver_params(ast_manager const & m, params_ref & p, bo
} }
ast_manager * context_params::mk_ast_manager() { ast_manager * context_params::mk_ast_manager() {
ast_manager * r = alloc(ast_manager, ast_manager * r = alloc(ast_manager,
m_proof ? PGM_FINE : PGM_DISABLED, m_proof ? PGM_FINE : PGM_DISABLED,
m_trace ? m_trace_file_name.c_str() : 0); m_trace ? m_trace_file_name.c_str() : 0);
if (m_smtlib2_compliant) if (m_smtlib2_compliant)
r->enable_int_real_coercions(false); r->enable_int_real_coercions(false);

7
src/cmd_context/context_params.h
View file

@ -25,7 +25,8 @@ class ast_manager;
class context_params { class context_params {
void set_bool(bool & opt, char const * param, char const * value); void set_bool(bool & opt, char const * param, char const * value);
void set_uint(unsigned & opt, char const * param, char const * value);
public: public:
bool m_auto_config; bool m_auto_config;
bool m_proof; bool m_proof;
@ -50,7 +51,7 @@ public:
/* /*
REG_PARAMS('context_params::collect_param_descrs') REG_PARAMS('context_params::collect_param_descrs')
*/ */
/** /**
\brief Goodies for extracting parameters for creating a solver object. \brief Goodies for extracting parameters for creating a solver object.
*/ */
@ -64,7 +65,7 @@ public:
Example: auto_config Example: auto_config
*/ */
params_ref merge_default_params(params_ref const & p); params_ref merge_default_params(params_ref const & p);
/** /**
\brief Create an AST manager using this configuration. \brief Create an AST manager using this configuration.
*/ */