Do not invoke memset with count of zero (#4205)

We need to apply similar exclusion rules as we already do for intrinsics
that invoke `memcmp`.

Resolves: #90
Resolves: #3772

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: tautschnig

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

@@ -1730,15 +1730,20 @@ impl GotocCtx<'_> {
 
         // Check that computing `count` in bytes would not overflow
         let (count_bytes, overflow_check) = self.count_in_bytes(
-            count,
+            count.clone(),
             pointee_type_stable(dst_typ).unwrap(),
             Type::size_t(),
             "write_bytes",
             loc,
         );
 
         let memset_call = BuiltinFn::Memset.call(vec![dst, val, count_bytes], loc);
-        Stmt::block(vec![align_check, overflow_check, memset_call.as_stmt(loc)], loc)
+        Stmt::if_then_else(
+            count.clone().gt(Expr::int_constant(0, count.typ().clone())),
+            Stmt::block(vec![align_check, overflow_check, memset_call.as_stmt(loc)], loc),
+            None,
+            loc,
+        )
     }
 
     /// Computes (multiplies) the equivalent of a memory-related number (e.g., an offset) in bytes.

tests/kani/NondetVectors/fixme_main.rs renamed to tests/kani/NondetVectors/main.rs

@@ -16,3 +16,20 @@ fn main() {
         assert!(_buf2[idx] == elt);
     }
 }
+
+#[kani::proof]
+fn minimal1() {
+    let v: Vec<i8> = vec![kani::any(); 0];
+}
+
+#[kani::proof]
+fn minimal2() {
+    let v: Vec<i8> = vec![5; 0];
+}
+
+#[kani::proof]
+fn vec3772() {
+    let value: u8 = 1; /* set to zero and it passes */
+    let count: u16 = kani::any();
+    let vector: Vec<u8> = vec![value; count as usize];
+}