Add a couple of missing tests (nondet. vectors, offset) (rust-lang#79)

* Add a couple of missing tests (nondet. vectors, offset)

* Add `test_offset_str` to BinOp_Offset test

* Add assertions in `NondetVectors` test

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

Author: 2 people

rust-tests/cbmc-reg/BinOp_Offset/main.rs

@@ -1,6 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-pub fn test_offset() {
+pub fn test_offset_array() {
     let s = ['a', 'b', 'c'];
     let ptr = s.as_ptr();
 
@@ -11,6 +11,18 @@ pub fn test_offset() {
     }
 }
 
+pub fn test_offset_str() {
+    let s: &str = "123";
+    let ptr: *const u8 = s.as_ptr();
+
+    unsafe {
+        assert!(*ptr.offset(0) == b'1');
+        assert!(*ptr.offset(1) == b'2');
+        assert!(*ptr.offset(2) == b'3');
+    }
+}
+
 pub fn main() {
-    test_offset();
+    test_offset_array();
+    test_offset_str()
 }

rust-tests/cbmc-reg/NondetVectors/fixme_main.rs

@@ -0,0 +1,21 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+const FIFO_SIZE: usize = 2;
+fn __nondet<T>() -> T {
+    unimplemented!()
+}
+
+fn main() {
+    let len: usize = __nondet();
+    if !(len <= FIFO_SIZE) {
+        return;
+    }
+    let _buf1: Vec<u8> = vec![0u8; len]; //< this works
+    let elt: u8 = __nondet();
+    let _buf2: Vec<u8> = vec![elt; len]; //< this fails: "memset destination region writeable"
+    let idx: usize = __nondet();
+    if idx < len {
+        assert!(_buf1[idx] == 0u8);
+        assert!(_buf2[idx] == elt);
+    }
+}