Ugly commit 26.14.

viperproject · Jun 24, 2023 · a2f371c · a2f371c
1 parent d899720
commit a2f371c
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 7 deletions.
diff --git a/prusti-viper/src/encoder/mir/places/interface.rs b/prusti-viper/src/encoder/mir/places/interface.rs
@@ -549,9 +549,10 @@ impl<'v, 'tcx: 'v> PlacesEncoderInterface<'tcx> for super::super::super::Encoder
                     );
                     return Ok(call);
                 } else {
-                    // Don't check the cast
-                    encoded_operand.set_type(destination_type);
-                    encoded_operand
+                    unimplemented!("Not checking overflows is currently not supported.");
+                    // // Don't check the cast
+                    // encoded_operand.set_type(destination_type);
+                    // encoded_operand
                 }
             }
 

diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs b/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs
@@ -922,7 +922,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     expression,
                     &broken_invariants,
                 )?;
-                assert!(!expression.find(result), "TODO: A proper error message that postconditions must not contain the result ({:?}): {expression}", procedure_contract.def_id);
+                assert!(!expression.find(result), "TODO: A proper error message that structural postconditions must not contain the result ({:?}): {expression}", procedure_contract.def_id);
                 postconditions.push(expression);
             }
         }

diff --git a/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs b/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs
@@ -999,12 +999,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ExpressionBackwardInterpreter<'p, 'v, 'tcx> {
             "std::ptr::const_ptr::<impl *const T>::offset"
             | "std::ptr::mut_ptr::<impl *mut T>::offset" => {
                 assert_eq!(encoded_args.len(), 2);
-                builtin((PtrWrappingOffset, encoded_args[0].get_type().clone()))
+                builtin((PtrOffset, encoded_args[0].get_type().clone()))
             }
             "std::ptr::const_ptr::<impl *const T>::wrapping_offset"
             | "std::ptr::mut_ptr::<impl *mut T>::wrapping_offset" => {
                 assert_eq!(encoded_args.len(), 2);
-                builtin((PtrOffset, encoded_args[0].get_type().clone()))
+                builtin((PtrWrappingOffset, encoded_args[0].get_type().clone()))
             }
             "std::ptr::const_ptr::<impl *const T>::add"
             | "std::ptr::mut_ptr::<impl *mut T>::add" => {

diff --git a/scripts/verify_test.py b/scripts/verify_test.py
@@ -142,7 +142,7 @@ def verify_test(args):
     report("Found test: {}", test_path)
     compile_flags = extract_test_compile_flags(test_path)
     env = get_env()
-    if 'prusti-tests/tests/verify_overflow/' in test_path:
+    if 'prusti-tests/tests/verify_overflow/' in test_path or 'prusti-tests/tests/verify_overflow_core_proof/' in test_path:
         env['PRUSTI_CHECK_OVERFLOWS'] = 'true'
     else:
         env['PRUSTI_CHECK_OVERFLOWS'] = 'false'