From 7cc466f9f6efb0eee4e985cb2336df1ddd9dd287 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Fri, 26 Jul 2024 19:38:03 +0000
Subject: [PATCH] Fix default safe body for unnamed fields

---
 library/kani_macros/src/derive.rs | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs
index 1d3b61b93a0e..2761fa8f5339 100644
--- a/library/kani_macros/src/derive.rs
+++ b/library/kani_macros/src/derive.rs
@@ -218,8 +218,25 @@ fn safe_body_default_inner(_ident: &Ident, fields: &Fields) -> TokenStream {
                 quote! { true }
             }
         }
-        Fields::Unnamed(_) => quote! {},
-        Fields::Unit => quote! {},
+        Fields::Unnamed(ref fields) => {
+            let field_safe_calls: Vec<TokenStream> = fields
+                .unnamed
+                .iter()
+                .enumerate()
+                .map(|(idx, field)| {
+                    let field_idx = Index::from(idx);
+                    quote_spanned! {field.span()=>
+                        #field_idx.is_safe()
+                    }
+                })
+                .collect();
+            if !field_safe_calls.is_empty() {
+                quote! { #( #field_safe_calls )&&* }
+            } else {
+                quote! { true }
+            }
+        }
+        Fields::Unit => quote! { true },
     }
 }