From 084a3daf976c78084fc61c4a7dc694a1608bae5a Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Tue, 3 Dec 2024 16:21:13 +0100 Subject: [PATCH] `allow(unused_variables)` instead of `let _ = x` --- creusot-contracts/src/logic/int.rs | 34 +++++++++---------- .../creusot-contracts/creusot-contracts.coma | 24 ++++++------- 2 files changed, 29 insertions(+), 29 deletions(-) diff --git a/creusot-contracts/src/logic/int.rs b/creusot-contracts/src/logic/int.rs index ac8fa5a040..b15a2ffc1d 100644 --- a/creusot-contracts/src/logic/int.rs +++ b/creusot-contracts/src/logic/int.rs @@ -59,8 +59,8 @@ impl Int { #[pure] #[ensures(*result == value@)] #[allow(unreachable_code)] + #[allow(unused_variables)] pub fn new(value: i128) -> GhostBox { - let _ = value; ghost!(panic!()) } @@ -75,8 +75,8 @@ impl Int { #[trusted] #[logic] #[creusot::builtins = "int.Power.power"] + #[allow(unused_variables)] pub fn pow(self, p: Int) -> Int { - let _ = p; dead } @@ -91,8 +91,8 @@ impl Int { #[trusted] #[logic] #[creusot::builtins = "int.MinMax.max"] + #[allow(unused_variables)] pub fn max(self, x: Int) -> Int { - let _ = x; dead } @@ -107,8 +107,8 @@ impl Int { #[logic] #[creusot::builtins = "int.MinMax.min"] #[trusted] + #[allow(unused_variables)] pub fn min(self, x: Int) -> Int { - let _ = x; dead } @@ -123,8 +123,8 @@ impl Int { #[trusted] #[logic] #[creusot::builtins = "int.EuclideanDivision.div"] + #[allow(unused_variables)] pub fn div_euclid(self, d: Int) -> Int { - let _ = d; dead } @@ -139,8 +139,8 @@ impl Int { #[trusted] #[logic] #[creusot::builtins = "int.EuclideanDivision.mod"] + #[allow(unused_variables)] pub fn rem_euclid(self, d: Int) -> Int { - let _ = d; dead } @@ -171,8 +171,8 @@ impl AddLogic for Int { #[trusted] #[creusot::no_translate] #[creusot::builtins = "add_int"] + #[allow(unused_variables)] fn add(self, other: Self) -> Self { - let _ = other; dead } } @@ -183,8 +183,8 @@ impl SubLogic for Int { #[trusted] #[creusot::no_translate] #[creusot::builtins = "sub_int"] + #[allow(unused_variables)] fn sub(self, other: Self) -> Self { - let _ = other; dead } } @@ -195,8 +195,8 @@ impl MulLogic for Int { #[trusted] #[creusot::no_translate] #[creusot::builtins = "mul_int"] + #[allow(unused_variables)] fn mul(self, other: Self) -> Self { - let _ = other; dead } } @@ -207,8 +207,8 @@ impl DivLogic for Int { #[trusted] #[creusot::no_translate] #[creusot::builtins = "div_int"] + #[allow(unused_variables)] fn div(self, other: Self) -> Self { - let _ = other; dead } } @@ -219,8 +219,8 @@ impl RemLogic for Int { #[trusted] #[creusot::no_translate] #[creusot::builtins = "rem_int"] + #[allow(unused_variables)] fn rem(self, other: Self) -> Self { - let _ = other; dead } } @@ -242,8 +242,8 @@ impl PartialEq for Int { #[trusted] #[pure] #[ensures(result == (*self == *other))] + #[allow(unused_variables)] fn eq(&self, other: &Self) -> bool { - let _ = other; unreachable!("BUG: called ghost function in normal code") } } @@ -253,8 +253,8 @@ impl Add for Int { #[trusted] #[pure] #[ensures(result == self + other)] + #[allow(unused_variables)] fn add(self, other: Int) -> Self { - let _ = other; unreachable!("BUG: called ghost function in normal code") } } @@ -264,8 +264,8 @@ impl Sub for Int { #[trusted] #[pure] #[ensures(result == self - other)] + #[allow(unused_variables)] fn sub(self, other: Int) -> Self { - let _ = other; unreachable!("BUG: called ghost function in normal code") } } @@ -275,8 +275,8 @@ impl Mul for Int { #[trusted] #[pure] #[ensures(result == self * other)] + #[allow(unused_variables)] fn mul(self, other: Int) -> Self { - let _ = other; unreachable!("BUG: called ghost function in normal code") } } @@ -286,8 +286,8 @@ impl Div for Int { #[trusted] #[pure] #[ensures(result == self / other)] + #[allow(unused_variables)] fn div(self, other: Int) -> Self { - let _ = other; unreachable!("BUG: called ghost function in normal code") } } @@ -297,8 +297,8 @@ impl Rem for Int { #[trusted] #[pure] #[ensures(result == self % other)] + #[allow(unused_variables)] fn rem(self, other: Int) -> Self { - let _ = other; unreachable!("BUG: called ghost function in normal code") } } diff --git a/creusot/tests/creusot-contracts/creusot-contracts.coma b/creusot/tests/creusot-contracts/creusot-contracts.coma index dda7dcb8a3..8748b1839a 100644 --- a/creusot/tests/creusot-contracts/creusot-contracts.coma +++ b/creusot/tests/creusot-contracts/creusot-contracts.coma @@ -27415,8 +27415,8 @@ module M_creusot_contracts__ghost__qyi17214052996668775070__deref_mut__refines [ = Borrow.borrow_logic (self.current).t_GhostBox__0'0 (self.final).t_GhostBox__0'0 (Borrow.inherit_id (Borrow.get_id self) 1) /\ inv'1 result -> inv'1 result) end -module M_creusot_contracts__logic__int__qyi8495612394334423323__eq__refines [#"../../../creusot-contracts/src/logic/int.rs" 245 4 245 38] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 245 4 245 38 +module M_creusot_contracts__logic__int__qyi8495612394334423323__eq__refines [#"../../../creusot-contracts/src/logic/int.rs" 246 4 246 38] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 246 4 246 38 let%span smodel1 = "../../../creusot-contracts/src/model.rs" 79 8 79 28 let%span smodel2 = "../../../creusot-contracts/src/model.rs" 126 8 126 12 @@ -27437,8 +27437,8 @@ module M_creusot_contracts__logic__int__qyi8495612394334423323__eq__refines [#". goal refines : [%#sint0] forall self : int . forall other : int . inv'0 other /\ inv'0 self -> (forall result : bool . result = (self = other) -> result = (deep_model'0 self = deep_model'0 other)) end -module M_creusot_contracts__logic__int__qyi3411234291730139970__add__refines [#"../../../creusot-contracts/src/logic/int.rs" 256 4 256 36] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 256 4 256 36 +module M_creusot_contracts__logic__int__qyi3411234291730139970__add__refines [#"../../../creusot-contracts/src/logic/int.rs" 257 4 257 36] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 257 4 257 36 use prelude.prelude.Int @@ -27449,8 +27449,8 @@ module M_creusot_contracts__logic__int__qyi3411234291730139970__add__refines [#" goal refines : [%#sint0] forall self : int . forall rhs : int . inv'0 rhs /\ inv'0 self -> (forall result : int . result = self + rhs -> inv'0 result) end -module M_creusot_contracts__logic__int__qyi14674898037351238599__sub__refines [#"../../../creusot-contracts/src/logic/int.rs" 267 4 267 36] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 267 4 267 36 +module M_creusot_contracts__logic__int__qyi14674898037351238599__sub__refines [#"../../../creusot-contracts/src/logic/int.rs" 268 4 268 36] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 268 4 268 36 use prelude.prelude.Int @@ -27461,8 +27461,8 @@ module M_creusot_contracts__logic__int__qyi14674898037351238599__sub__refines [# goal refines : [%#sint0] forall self : int . forall rhs : int . inv'0 rhs /\ inv'0 self -> (forall result : int . result = self - rhs -> inv'0 result) end -module M_creusot_contracts__logic__int__qyi92031444461445902__mul__refines [#"../../../creusot-contracts/src/logic/int.rs" 278 4 278 36] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 278 4 278 36 +module M_creusot_contracts__logic__int__qyi92031444461445902__mul__refines [#"../../../creusot-contracts/src/logic/int.rs" 279 4 279 36] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 279 4 279 36 use prelude.prelude.Int @@ -27473,8 +27473,8 @@ module M_creusot_contracts__logic__int__qyi92031444461445902__mul__refines [#".. goal refines : [%#sint0] forall self : int . forall rhs : int . inv'0 rhs /\ inv'0 self -> (forall result : int . result = self * rhs -> inv'0 result) end -module M_creusot_contracts__logic__int__qyi2704776725966497021__div__refines [#"../../../creusot-contracts/src/logic/int.rs" 289 4 289 36] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 289 4 289 36 +module M_creusot_contracts__logic__int__qyi2704776725966497021__div__refines [#"../../../creusot-contracts/src/logic/int.rs" 290 4 290 36] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 290 4 290 36 use prelude.prelude.Int @@ -27485,8 +27485,8 @@ module M_creusot_contracts__logic__int__qyi2704776725966497021__div__refines [#" goal refines : [%#sint0] forall self : int . forall rhs : int . inv'0 rhs /\ inv'0 self -> (forall result : int . result = div self rhs -> inv'0 result) end -module M_creusot_contracts__logic__int__qyi13390566486180286353__rem__refines [#"../../../creusot-contracts/src/logic/int.rs" 300 4 300 36] (* *) - let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 300 4 300 36 +module M_creusot_contracts__logic__int__qyi13390566486180286353__rem__refines [#"../../../creusot-contracts/src/logic/int.rs" 301 4 301 36] (* *) + let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 301 4 301 36 use prelude.prelude.Int