Skip to content

Commit

Permalink
Fix CI (#329)
Browse files Browse the repository at this point in the history
* Update emscripten

* Bump z3 submodule to new release

* Pin to cc 1.1 for now

* Add expect lint annotation

* Elide lifetimes

* Add note on cc pinning

* Use allow instead of expect to avoid de-facto MSRV bump
  • Loading branch information
toolCHAINZ authored Dec 9, 2024
1 parent 60001b3 commit 4f9fcfe
Show file tree
Hide file tree
Showing 17 changed files with 57 additions and 53 deletions.
3 changes: 3 additions & 0 deletions z3-sys/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,9 @@ repository = "https://github.com/prove-rs/z3.rs.git"

[build-dependencies]
bindgen = { version = "0.70", default-features = false, features = ["runtime"] }
# Temporarily pinning cc to 1.1 as 1.2 and later use -fno-exceptions, which
# breaks the z3 build. See https://github.com/prove-rs/z3.rs/issues/328
cc = "~1.1"
cmake = { version = "0.1.49", optional = true }
pkg-config = "0.3.27"
vcpkg = { version = "0.2.15", optional = true }
Expand Down
1 change: 1 addition & 0 deletions z3/src/ast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2317,6 +2317,7 @@ pub fn exists_const<'ctx>(
/// let f_f_3: ast::Int = f.apply(&[&f.apply(&[&ast::Int::from_u64(&ctx, 3)])]).try_into().unwrap();
/// assert_eq!(3, model.eval(&f_f_3, true).unwrap().as_u64().unwrap());
/// ```
#[allow(clippy::too_many_arguments)]
pub fn quantifier_const<'ctx>(
ctx: &'ctx Context,
is_forall: bool,
Expand Down
6 changes: 3 additions & 3 deletions z3/src/context.rs
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ impl Context {
}
}

impl<'ctx> ContextHandle<'ctx> {
impl ContextHandle<'_> {
/// Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
pub fn interrupt(&self) {
unsafe {
Expand All @@ -68,8 +68,8 @@ impl<'ctx> ContextHandle<'ctx> {
}
}

unsafe impl<'ctx> Sync for ContextHandle<'ctx> {}
unsafe impl<'ctx> Send for ContextHandle<'ctx> {}
unsafe impl Sync for ContextHandle<'_> {}
unsafe impl Send for ContextHandle<'_> {}

impl Drop for Context {
fn drop(&mut self) {
Expand Down
6 changes: 3 additions & 3 deletions z3/src/func_decl.rs
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ impl<'ctx> FuncDecl<'ctx> {
}
}

impl<'ctx> fmt::Display for FuncDecl<'ctx> {
impl fmt::Display for FuncDecl<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
let p = unsafe { Z3_func_decl_to_string(self.ctx.z3_ctx, self.z3_func_decl) };
if p.is_null() {
Expand All @@ -112,13 +112,13 @@ impl<'ctx> fmt::Display for FuncDecl<'ctx> {
}
}

impl<'ctx> fmt::Debug for FuncDecl<'ctx> {
impl fmt::Debug for FuncDecl<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
<Self as fmt::Display>::fmt(self, f)
}
}

impl<'ctx> Drop for FuncDecl<'ctx> {
impl Drop for FuncDecl<'_> {
fn drop(&mut self) {
unsafe {
Z3_dec_ref(
Expand Down
6 changes: 3 additions & 3 deletions z3/src/func_entry.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ impl<'ctx> FuncEntry<'ctx> {
}
}

impl<'ctx> fmt::Display for FuncEntry<'ctx> {
impl fmt::Display for FuncEntry<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
write!(f, "[")?;
self.get_args()
Expand All @@ -52,13 +52,13 @@ impl<'ctx> fmt::Display for FuncEntry<'ctx> {
}
}

impl<'ctx> fmt::Debug for FuncEntry<'ctx> {
impl fmt::Debug for FuncEntry<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
<Self as fmt::Display>::fmt(self, f)
}
}

impl<'ctx> Drop for FuncEntry<'ctx> {
impl Drop for FuncEntry<'_> {
fn drop(&mut self) {
unsafe {
Z3_func_entry_dec_ref(self.ctx.z3_ctx, self.z3_func_entry);
Expand Down
6 changes: 3 additions & 3 deletions z3/src/func_interp.rs
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ impl<'ctx> FuncInterp<'ctx> {
}
}

impl<'ctx> fmt::Display for FuncInterp<'ctx> {
impl fmt::Display for FuncInterp<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
write!(f, "[")?;
self.get_entries().into_iter().try_for_each(|e| {
Expand All @@ -95,13 +95,13 @@ impl<'ctx> fmt::Display for FuncInterp<'ctx> {
}
}

impl<'ctx> fmt::Debug for FuncInterp<'ctx> {
impl fmt::Debug for FuncInterp<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
<Self as fmt::Display>::fmt(self, f)
}
}

impl<'ctx> Drop for FuncInterp<'ctx> {
impl Drop for FuncInterp<'_> {
fn drop(&mut self) {
unsafe {
Z3_func_interp_dec_ref(self.ctx.z3_ctx, self.z3_func_interp);
Expand Down
8 changes: 4 additions & 4 deletions z3/src/goal.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ use z3_sys::*;

use crate::{ast, ast::Ast, Context, Goal};

impl<'ctx> Clone for Goal<'ctx> {
impl Clone for Goal<'_> {
fn clone(&self) -> Self {
Self {
ctx: self.ctx,
Expand Down Expand Up @@ -109,7 +109,7 @@ impl<'ctx> Goal<'ctx> {
}
}

impl<'ctx> fmt::Display for Goal<'ctx> {
impl fmt::Display for Goal<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
let p = unsafe { Z3_goal_to_string(self.ctx.z3_ctx, self.z3_goal) };
if p.is_null() {
Expand All @@ -122,13 +122,13 @@ impl<'ctx> fmt::Display for Goal<'ctx> {
}
}

impl<'ctx> fmt::Debug for Goal<'ctx> {
impl fmt::Debug for Goal<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
<Self as fmt::Display>::fmt(self, f)
}
}

impl<'ctx> Drop for Goal<'ctx> {
impl Drop for Goal<'_> {
fn drop(&mut self) {
unsafe {
Z3_goal_dec_ref(self.ctx.z3_ctx, self.z3_goal);
Expand Down
8 changes: 4 additions & 4 deletions z3/src/model.rs
Original file line number Diff line number Diff line change
Expand Up @@ -135,7 +135,7 @@ impl<'ctx> Model<'ctx> {
}
}

impl<'ctx> fmt::Display for Model<'ctx> {
impl fmt::Display for Model<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
let p = unsafe { Z3_model_to_string(self.ctx.z3_ctx, self.z3_mdl) };
if p.is_null() {
Expand All @@ -148,13 +148,13 @@ impl<'ctx> fmt::Display for Model<'ctx> {
}
}

impl<'ctx> fmt::Debug for Model<'ctx> {
impl fmt::Debug for Model<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
<Self as fmt::Display>::fmt(self, f)
}
}

impl<'ctx> Drop for Model<'ctx> {
impl Drop for Model<'_> {
fn drop(&mut self) {
unsafe { Z3_model_dec_ref(self.ctx.z3_ctx, self.z3_mdl) };
}
Expand All @@ -181,7 +181,7 @@ impl<'a, 'ctx> IntoIterator for &'a Model<'ctx> {
}
}

impl<'a, 'ctx> Iterator for ModelIter<'a, 'ctx> {
impl<'ctx> Iterator for ModelIter<'_, 'ctx> {
type Item = FuncDecl<'ctx>;

fn next(&mut self) -> Option<Self::Item> {
Expand Down
6 changes: 3 additions & 3 deletions z3/src/optimize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -274,7 +274,7 @@ impl<'ctx> Optimize<'ctx> {
}
}

impl<'ctx> fmt::Display for Optimize<'ctx> {
impl fmt::Display for Optimize<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
let p = unsafe { Z3_optimize_to_string(self.ctx.z3_ctx, self.z3_opt) };
if p.is_null() {
Expand All @@ -287,13 +287,13 @@ impl<'ctx> fmt::Display for Optimize<'ctx> {
}
}

impl<'ctx> fmt::Debug for Optimize<'ctx> {
impl fmt::Debug for Optimize<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
<Self as fmt::Display>::fmt(self, f)
}
}

impl<'ctx> Drop for Optimize<'ctx> {
impl Drop for Optimize<'_> {
fn drop(&mut self) {
unsafe { Z3_optimize_dec_ref(self.ctx.z3_ctx, self.z3_opt) };
}
Expand Down
6 changes: 3 additions & 3 deletions z3/src/params.rs
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ pub fn reset_all_global_params() {
unsafe { Z3_global_param_reset_all() };
}

impl<'ctx> fmt::Display for Params<'ctx> {
impl fmt::Display for Params<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
let p = unsafe { Z3_params_to_string(self.ctx.z3_ctx, self.z3_params) };
if p.is_null() {
Expand All @@ -112,13 +112,13 @@ impl<'ctx> fmt::Display for Params<'ctx> {
}
}

impl<'ctx> fmt::Debug for Params<'ctx> {
impl fmt::Debug for Params<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
<Self as fmt::Display>::fmt(self, f)
}
}

impl<'ctx> Drop for Params<'ctx> {
impl Drop for Params<'_> {
fn drop(&mut self) {
unsafe { Z3_params_dec_ref(self.ctx.z3_ctx, self.z3_params) };
}
Expand Down
6 changes: 3 additions & 3 deletions z3/src/pattern.rs
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ impl<'ctx> Pattern<'ctx> {
}
}

impl<'ctx> fmt::Debug for Pattern<'ctx> {
impl fmt::Debug for Pattern<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
let p = unsafe { Z3_pattern_to_string(self.ctx.z3_ctx, self.z3_pattern) };
if p.is_null() {
Expand All @@ -59,13 +59,13 @@ impl<'ctx> fmt::Debug for Pattern<'ctx> {
}
}

impl<'ctx> fmt::Display for Pattern<'ctx> {
impl fmt::Display for Pattern<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
<Self as fmt::Debug>::fmt(self, f)
}
}

impl<'ctx> Drop for Pattern<'ctx> {
impl Drop for Pattern<'_> {
fn drop(&mut self) {
unsafe {
Z3_dec_ref(self.ctx.z3_ctx, self.z3_pattern as Z3_ast);
Expand Down
8 changes: 4 additions & 4 deletions z3/src/probe.rs
Original file line number Diff line number Diff line change
Expand Up @@ -167,25 +167,25 @@ impl<'ctx> Probe<'ctx> {
}
}

impl<'ctx> Clone for Probe<'ctx> {
impl Clone for Probe<'_> {
fn clone(&self) -> Self {
unsafe { Self::wrap(self.ctx, self.z3_probe) }
}
}

impl<'ctx> fmt::Display for Probe<'ctx> {
impl fmt::Display for Probe<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
write!(f, "<z3.probe>")
}
}

impl<'ctx> fmt::Debug for Probe<'ctx> {
impl fmt::Debug for Probe<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
<Self as fmt::Display>::fmt(self, f)
}
}

impl<'ctx> Drop for Probe<'ctx> {
impl Drop for Probe<'_> {
fn drop(&mut self) {
unsafe {
Z3_probe_dec_ref(self.ctx.z3_ctx, self.z3_probe);
Expand Down
6 changes: 3 additions & 3 deletions z3/src/rec_func_decl.rs
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ impl<'ctx> RecFuncDecl<'ctx> {
}
}

impl<'ctx> fmt::Display for RecFuncDecl<'ctx> {
impl fmt::Display for RecFuncDecl<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
let p = unsafe { Z3_func_decl_to_string(self.ctx.z3_ctx, self.z3_func_decl) };
if p.is_null() {
Expand All @@ -107,13 +107,13 @@ impl<'ctx> fmt::Display for RecFuncDecl<'ctx> {
}
}

impl<'ctx> fmt::Debug for RecFuncDecl<'ctx> {
impl fmt::Debug for RecFuncDecl<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
<Self as fmt::Display>::fmt(self, f)
}
}

impl<'ctx> Drop for RecFuncDecl<'ctx> {
impl Drop for RecFuncDecl<'_> {
fn drop(&mut self) {
unsafe {
Z3_dec_ref(
Expand Down
6 changes: 3 additions & 3 deletions z3/src/solver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -400,7 +400,7 @@ impl<'ctx> Solver<'ctx> {
}
}

impl<'ctx> fmt::Display for Solver<'ctx> {
impl fmt::Display for Solver<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
let p = unsafe { Z3_solver_to_string(self.ctx.z3_ctx, self.z3_slv) };
if p.is_null() {
Expand All @@ -413,13 +413,13 @@ impl<'ctx> fmt::Display for Solver<'ctx> {
}
}

impl<'ctx> fmt::Debug for Solver<'ctx> {
impl fmt::Debug for Solver<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
<Self as fmt::Display>::fmt(self, f)
}
}

impl<'ctx> Drop for Solver<'ctx> {
impl Drop for Solver<'_> {
fn drop(&mut self) {
unsafe { Z3_solver_dec_ref(self.ctx.z3_ctx, self.z3_slv) };
}
Expand Down
12 changes: 6 additions & 6 deletions z3/src/sort.rs
Original file line number Diff line number Diff line change
Expand Up @@ -274,13 +274,13 @@ impl<'ctx> Sort<'ctx> {
}
}

impl<'ctx> Clone for Sort<'ctx> {
impl Clone for Sort<'_> {
fn clone(&self) -> Self {
unsafe { Self::wrap(self.ctx, self.z3_sort) }
}
}

impl<'ctx> fmt::Display for Sort<'ctx> {
impl fmt::Display for Sort<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
let p = unsafe { Z3_sort_to_string(self.ctx.z3_ctx, self.z3_sort) };
if p.is_null() {
Expand All @@ -293,7 +293,7 @@ impl<'ctx> fmt::Display for Sort<'ctx> {
}
}

impl<'ctx> fmt::Debug for Sort<'ctx> {
impl fmt::Debug for Sort<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
<Self as fmt::Display>::fmt(self, f)
}
Expand All @@ -305,9 +305,9 @@ impl<'ctx> PartialEq<Sort<'ctx>> for Sort<'ctx> {
}
}

impl<'ctx> Eq for Sort<'ctx> {}
impl Eq for Sort<'_> {}

impl<'ctx> Drop for Sort<'ctx> {
impl Drop for Sort<'_> {
fn drop(&mut self) {
unsafe {
Z3_dec_ref(
Expand All @@ -332,7 +332,7 @@ impl<'ctx> SortDiffers<'ctx> {
}
}

impl<'ctx> fmt::Display for SortDiffers<'ctx> {
impl fmt::Display for SortDiffers<'_> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
write!(
f,
Expand Down
Loading

0 comments on commit 4f9fcfe

Please sign in to comment.