From 519ff34d4e4a8e0d8f9c1f5beef217254df66c1c Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Mon, 25 Mar 2024 14:29:30 +0100 Subject: [PATCH] Add regression test for issue #1505 --- .../verify_overflow/fail/issues/issue-1505.rs | 43 +++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs diff --git a/prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs b/prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs new file mode 100644 index 00000000000..4a42eda82a1 --- /dev/null +++ b/prusti-tests/tests/verify_overflow/fail/issues/issue-1505.rs @@ -0,0 +1,43 @@ +use prusti_contracts::*; + +// To inhibit constant-propagation optimizations: +#[pure] +fn id(x: T) -> T { x} + +fn check_division(){ + assert!(id(3i32) / 2 == 1); + assert!(id(-3i32) / 2 == -1); + assert!(id(3i32) / -2 == -1); + assert!(id(-3i32) / -2 == 1); + prusti_assert!(id(3i32) / 2 == 1); + prusti_assert!(id(-3i32) / 2 == -1); + prusti_assert!(id(3i32) / -2 == -1); + prusti_assert!(id(-3i32) / -2 == 1); + + // Smoke test + assert!(false); //~ ERROR the asserted expression might not hold +} + +fn check_modulo() { + assert!(id(10) % 3 == 1); + assert!(id(10) % -3 == 1); + assert!(id(-10) % 3 == -1); + assert!(id(-10) % -3 == -1); + + assert!(id(3) % 3 == 0); + assert!(id(2) % 3 == 2); + assert!(id(1) % 3 == 1); + assert!(id(0) % 3 == 0); + assert!(id(-1) % 3 == -1); + assert!(id(-2) % 3 == -2); + assert!(id(-3) % 3 == 0); + assert!(id(-4) % 3 == -1); + assert!(id(-5) % 3 == -2); + + assert!(id(-4) % 2 == 0); + + // Smoke test + assert!(false); //~ ERROR the asserted expression might not hold +} + +fn main(){}