From 4e59ba922b356429482e25389206d3dd6e745124 Mon Sep 17 00:00:00 2001 From: "Daniel J. Hofmann" Date: Fri, 3 Apr 2015 19:13:52 +0200 Subject: [PATCH 1/6] Wc++11-extensions --- src/api/z3_api.h | 2 +- src/ast/ast.h | 2 +- src/ast/pattern/expr_pattern_match.h | 2 +- src/smt/params/smt_params.h | 2 +- src/smt/smt_setup.h | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 844a4766c..45e5a9266 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -176,7 +176,7 @@ typedef enum Z3_PARAMETER_SYMBOL, Z3_PARAMETER_SORT, Z3_PARAMETER_AST, - Z3_PARAMETER_FUNC_DECL, + Z3_PARAMETER_FUNC_DECL } Z3_parameter_kind; /** diff --git a/src/ast/ast.h b/src/ast/ast.h index 93f456965..277e9120b 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1143,7 +1143,7 @@ typedef app proof; /* a proof is just an applicaton */ enum label_op_kind { OP_LABEL, - OP_LABEL_LIT, + OP_LABEL_LIT }; /** diff --git a/src/ast/pattern/expr_pattern_match.h b/src/ast/pattern/expr_pattern_match.h index 555d6a67e..c298c2992 100644 --- a/src/ast/pattern/expr_pattern_match.h +++ b/src/ast/pattern/expr_pattern_match.h @@ -37,7 +37,7 @@ class expr_pattern_match { CHECK_TERM, SET_BOUND, CHECK_BOUND, - YIELD, + YIELD }; struct instr { diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 2fbc9b6d4..dc1fc0911 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -65,7 +65,7 @@ enum case_split_strategy { CS_ACTIVITY_WITH_CACHE, // case split based on activity and cache the activity CS_RELEVANCY, // case split based on relevancy CS_RELEVANCY_ACTIVITY, // case split based on relevancy and activity - CS_RELEVANCY_GOAL, // based on relevancy and the current goal + CS_RELEVANCY_GOAL // based on relevancy and the current goal }; struct smt_params : public preprocessor_params, diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index 6cbcb9602..1a30f3722 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -28,7 +28,7 @@ namespace smt { enum config_mode { CFG_BASIC, // install theories based on user options CFG_LOGIC, // install theories and configure Z3 based on the value of the parameter set-logic. - CFG_AUTO, // install theories based on static features of the input formula + CFG_AUTO // install theories based on static features of the input formula }; class context; From 6150083276a1cb4d87e27e56c3a31397cf8807b9 Mon Sep 17 00:00:00 2001 From: "Daniel J. Hofmann" Date: Fri, 3 Apr 2015 19:24:35 +0200 Subject: [PATCH 2/6] Wignored-qualifiers --- src/muz/rel/dl_sparse_table.h | 2 +- src/util/hwf.h | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/muz/rel/dl_sparse_table.h b/src/muz/rel/dl_sparse_table.h index 0222aa6e2..4768d8862 100644 --- a/src/muz/rel/dl_sparse_table.h +++ b/src/muz/rel/dl_sparse_table.h @@ -350,7 +350,7 @@ namespace datalog { *ptr&=m_write_mask; *ptr|=val< { diff --git a/src/util/hwf.h b/src/util/hwf.h index 9059869a0..be8ad7e0e 100644 --- a/src/util/hwf.h +++ b/src/util/hwf.h @@ -127,15 +127,15 @@ public: void to_rational(hwf const & x, scoped_mpq & o) { to_rational(x, o.m(), o); } - bool sgn(hwf const & x) const { + bool sgn(hwf const & x) const { return (x.get_raw() & 0x8000000000000000ull) != 0; } - const uint64 sig(hwf const & x) const { + uint64 sig(hwf const & x) const { return x.get_raw() & 0x000FFFFFFFFFFFFFull; } - const int exp(hwf const & x) const { + int exp(hwf const & x) const { return ((x.get_raw() & 0x7FF0000000000000ull) >> 52) - 1023; } From 88f6e74a2741818649d00959276d82f12372fa57 Mon Sep 17 00:00:00 2001 From: "Daniel J. Hofmann" Date: Fri, 3 Apr 2015 19:31:09 +0200 Subject: [PATCH 3/6] Wnewline-eof --- src/ast/fpa_decl_plugin.cpp | 2 +- src/smt/params/dyn_ack_params.cpp | 2 +- src/tactic/fpa/fpa2bv_model_converter.h | 2 +- src/tactic/sls/sls_evaluator.h | 2 +- src/tactic/sls/sls_powers.h | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 48b7adb8b..1e8fbd3f6 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -1009,4 +1009,4 @@ app * fpa_util::mk_internal_to_sbv_unspecified(unsigned width) { app * fpa_util::mk_internal_to_real_unspecified() { sort * range = m_a_util.mk_real(); return m().mk_app(get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED, 0, 0, 0, 0, range); -} \ No newline at end of file +} diff --git a/src/smt/params/dyn_ack_params.cpp b/src/smt/params/dyn_ack_params.cpp index c559e2b9b..15f48bad1 100644 --- a/src/smt/params/dyn_ack_params.cpp +++ b/src/smt/params/dyn_ack_params.cpp @@ -27,4 +27,4 @@ void dyn_ack_params::updt_params(params_ref const & _p) { m_dack_threshold = p.dack_threshold(); m_dack_gc = p.dack_gc(); m_dack_gc_inv_decay = p.dack_gc_inv_decay(); -} \ No newline at end of file +} diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 7b9598740..dc3df0557 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -103,4 +103,4 @@ model_converter * mk_fpa2bv_model_converter(ast_manager & m, obj_map const & uf2bvuf, obj_map const & uf23bvuf); -#endif \ No newline at end of file +#endif diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 61afb7457..c70aba0d4 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -812,4 +812,4 @@ public: } }; -#endif \ No newline at end of file +#endif diff --git a/src/tactic/sls/sls_powers.h b/src/tactic/sls/sls_powers.h index d0cc0815e..bf28b80e9 100644 --- a/src/tactic/sls/sls_powers.h +++ b/src/tactic/sls/sls_powers.h @@ -46,4 +46,4 @@ public: } }; -#endif \ No newline at end of file +#endif From 42e0132639da1a3535a6e58299b514784e700205 Mon Sep 17 00:00:00 2001 From: "Daniel J. Hofmann" Date: Fri, 3 Apr 2015 19:45:49 +0200 Subject: [PATCH 4/6] Wshift-sign-overflow See: http://stackoverflow.com/questions/26331035/why-was-1-31-changed-to-be-implementation-defined-in-c14 And Howard Hinnant's explanation: http://stackoverflow.com/questions/19593938/is-left-shifting-a-negative-integer-undefined-behavior-in-c11#comment29091986_19593938 --- src/ast/ast.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index 277e9120b..1e33cc6d2 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -522,7 +522,7 @@ public: /** The ids of expressions and declarations are in different ranges. */ -const unsigned c_first_decl_id = (1 << 31); +const unsigned c_first_decl_id = (1u << 31); /** \brief Superclass for function declarations and sorts. From 2252836cf8d9d87027aae6137f7478efa4e338f1 Mon Sep 17 00:00:00 2001 From: "Daniel J. Hofmann" Date: Fri, 3 Apr 2015 19:53:13 +0200 Subject: [PATCH 5/6] Wstring-conversion static_cast("string lit") evaluates to true. The assert is supposed to always trigger, thus assert(false && "string lit"). --- src/interp/iz3foci.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp index 527e73ae4..fbb52a071 100755 --- a/src/interp/iz3foci.cpp +++ b/src/interp/iz3foci.cpp @@ -272,7 +272,7 @@ public: } break; default: - assert("unknown built-in op"); + assert(false && "unknown built-in op"); } } else if(foci->get_int(i,nval)){ From 4b6b7182227984a928ce616f19adce0b6571fad9 Mon Sep 17 00:00:00 2001 From: "Daniel J. Hofmann" Date: Fri, 3 Apr 2015 20:11:58 +0200 Subject: [PATCH 6/6] Wunused-exception-parameter --- src/muz/duality/duality_dl_interface.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index aa186bd0a..9227059aa 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -327,10 +327,10 @@ lbool dl_interface::query(::expr * query) { try { ans = rs->Solve(); } - catch (Duality::solver::cancel_exception &exn){ + catch (const Duality::solver::cancel_exception &){ throw default_exception("duality canceled"); } - catch (Duality::Solver::Incompleteness &exn){ + catch (const Duality::Solver::Incompleteness &){ throw default_exception("incompleteness"); }