Add nondet. bytes test (rust-lang#94)

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

Author: 2 people

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

@@ -0,0 +1,27 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+use std::convert::TryInto;
+
+fn __nondet<T>() -> T {
+    unimplemented!()
+}
+
+fn main() {
+    let input: &[u8] = &vec![
+        __nondet(),
+        __nondet(),
+        __nondet(),
+        __nondet(),
+        __nondet(),
+        __nondet(),
+        __nondet(),
+        __nondet(),
+    ];
+    let buffer = input.as_ref();
+    let bytes: [u8; 8] = buffer.try_into().unwrap();
+    let value = u64::from_be_bytes(bytes);
+    let idx: usize = __nondet();
+    if idx < 8 {
+        assert!(u64::to_be_bytes(value)[idx] == input[idx]);
+    }
+}