From f8e6ee9abb2bcd67bad3d1536163d22ddd95f2d9 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 22 Apr 2021 11:42:02 +0000
Subject: [PATCH] Add nondet. bytes test

---
 rust-tests/cbmc-reg/NondetVectors/bytes.rs | 27 ++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 rust-tests/cbmc-reg/NondetVectors/bytes.rs

diff --git a/rust-tests/cbmc-reg/NondetVectors/bytes.rs b/rust-tests/cbmc-reg/NondetVectors/bytes.rs
new file mode 100644
index 000000000000..a2c4276718f1
--- /dev/null
+++ b/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]);
+    }
+}