Parameters are not to be treated different

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -34,10 +34,11 @@ impl<'tcx> GotocCtx<'tcx> {
             let var_type = self.codegen_ty_stable(ldata.ty);
             let loc = self.codegen_span_stable(ldata.span);
             // Indices [1, N] represent the function parameters where N is the number of parameters.
+            // Except that ZST fields are not included as parameters.
             let sym =
                 Symbol::variable(name, base_name, var_type, self.codegen_span_stable(ldata.span))
                     .with_is_hidden(!self.is_user_variable(&lc))
-                    .with_is_parameter(lc > 0 && lc <= num_args);
+                    .with_is_parameter((lc > 0 && lc <= num_args) && !self.is_zst_stable(ldata.ty));
             let sym_e = sym.to_expr();
             self.symbol_table.insert(sym);
 
@@ -175,7 +176,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 let (name, base_name) = self.codegen_spread_arg_name(&lc);
                 let sym = Symbol::variable(name, base_name, self.codegen_ty_stable(*arg_t), loc)
                     .with_is_hidden(false)
-                    .with_is_parameter(true);
+                    .with_is_parameter(!self.is_zst_stable(*arg_t));
                 // The spread arguments are additional function paramaters that are patched in
                 // They are to the function signature added in the `fn_typ` function.
                 // But they were never added to the symbol table, which we currently do here.

kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

@@ -642,16 +642,15 @@ impl<'tcx> GotocCtx<'tcx> {
         let projection =
             unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(place));
         if self.use_thin_pointer_stable(place_ty) {
-            // For non-parameter objects with ZST rustc does not necessarily generate
-            // individual objects.
+            // For ZST objects rustc does not necessarily generate individual objects.
             let need_not_be_unique = match projection.goto_expr.value() {
-                ExprValue::Symbol { identifier } => {
-                    !self.symbol_table.lookup(*identifier).unwrap().is_parameter
+                ExprValue::Symbol { .. } => {
+                    self.is_zst_stable(place_ty)
                 }
                 _ => false,
             };
             let address_of = projection.goto_expr.address_of();
-            if need_not_be_unique && self.is_zst_stable(place_ty) {
+            if need_not_be_unique {
                 let global_zst_name = "__kani_zst_object";
                 let zst_typ = self.codegen_ty_stable(place_ty);
                 let global_zst_object = self.ensure_global_var(

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -137,7 +137,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     // Generate a Symbol Expression representing a function variable from the MIR
     pub fn gen_function_local_variable(&mut self, c: u64, fname: &str, t: Type) -> Symbol {
-        self.gen_stack_variable(c, fname, "var", t, Location::none())
+        self.gen_stack_variable(c, fname, "var", t, Location::none(), false)
     }
 
     /// Given a counter `c` a function name `fname, and a prefix `prefix`, generates a new function local variable
@@ -149,10 +149,11 @@ impl<'tcx> GotocCtx<'tcx> {
         prefix: &str,
         t: Type,
         loc: Location,
+        is_param: bool,
     ) -> Symbol {
         let base_name = format!("{prefix}_{c}");
         let name = format!("{fname}::1::{base_name}");
-        let symbol = Symbol::variable(name, base_name, t, loc);
+        let symbol = Symbol::variable(name, base_name, t, loc).with_is_parameter(is_param);
         self.symbol_table.insert(symbol.clone());
         symbol
     }
@@ -166,7 +167,8 @@ impl<'tcx> GotocCtx<'tcx> {
         loc: Location,
     ) -> (Expr, Stmt) {
         let c = self.current_fn_mut().get_and_incr_counter();
-        let var = self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc).to_expr();
+        let var =
+            self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc, false).to_expr();
         let value = value.or_else(|| self.codegen_default_initializer(&var));
         let decl = Stmt::decl(var.clone(), value, loc);
         (var, decl)

tests/kani/Closure/zst_param.rs

@@ -17,7 +17,8 @@ fn check_zst_param() {
     let input = kani::any();
     let closure = |a: Void, out: usize, b: Void| {
         kani::cover!();
-        assert!(&a as *const Void != &b as *const Void, "Should succeed");
+        assert!(&a as *const Void != std::ptr::null(), "Should succeed");
+        assert!(&b as *const Void != std::ptr::null(), "Should succeed");
         out
     };
     let output = invoke(input, closure);