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

don't crash in Z3_model_eval API if not given a valid expression

Browse source 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-06-26 18:33:13 +01:00
parent e81dc5a0a0
commit 3104d2954c
3 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/api/api_ast.cpp
View file

@ -664,12 +664,9 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_get_bool_value(c, a); LOG_Z3_get_bool_value(c, a);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_IS_EXPR(a, Z3_L_UNDEF);
ast_manager & m = mk_c(c)->m(); ast_manager & m = mk_c(c)->m();
ast * n = to_ast(a); ast * n = to_ast(a);
if (!is_expr(n)) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return Z3_L_UNDEF;
}
if (m.is_true(to_expr(n))) if (m.is_true(to_expr(n)))
return Z3_L_TRUE; return Z3_L_TRUE;
if (m.is_false(to_expr(n))) if (m.is_false(to_expr(n)))

1
src/api/api_context.h
View file

@ -244,6 +244,7 @@ inline api::context * mk_c(Z3_context c) { return reinterpret_cast<api::context*
#define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG); return _ret_; } } #define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG); return _ret_; } }
#define CHECK_SEARCHING(c) mk_c(c)->check_searching(); #define CHECK_SEARCHING(c) mk_c(c)->check_searching();
inline bool is_expr(Z3_ast a) { return is_expr(to_ast(a)); } inline bool is_expr(Z3_ast a) { return is_expr(to_ast(a)); }
#define CHECK_IS_EXPR(_p_, _ret_) { if (!is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG); return _ret_; } }
inline bool is_bool_expr(Z3_context c, Z3_ast a) { return is_expr(a) && mk_c(c)->m().is_bool(to_expr(a)); } inline bool is_bool_expr(Z3_context c, Z3_ast a) { return is_expr(a) && mk_c(c)->m().is_bool(to_expr(a)); }
#define CHECK_FORMULA(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG); return _ret_; } } #define CHECK_FORMULA(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG); return _ret_; } }
inline void check_sorts(Z3_context c, ast * n) { mk_c(c)->check_sorts(n); } inline void check_sorts(Z3_context c, ast * n) { mk_c(c)->check_sorts(n); }

1
src/api/api_model.cpp
View file

@ -153,6 +153,7 @@ extern "C" {
if (v) *v = 0; if (v) *v = 0;
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_NON_NULL(m, Z3_FALSE); CHECK_NON_NULL(m, Z3_FALSE);
CHECK_IS_EXPR(t, Z3_FALSE);
model * _m = to_model_ref(m); model * _m = to_model_ref(m);
expr_ref result(mk_c(c)->m()); expr_ref result(mk_c(c)->m());
_m->eval(to_expr(t), result, model_completion == Z3_TRUE); _m->eval(to_expr(t), result, model_completion == Z3_TRUE);