Cleanup links to issues that have been addressed (#4200)

Over time, some issues got fixed yet our comments still claimed there
was work to be done. Remove or replace these comments by more up-to-date
ones.

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

.github/workflows/extra_jobs.yml

@@ -15,7 +15,7 @@
 # Note that this also means that the workflow version run is the one currently in `main`,
 # not the one from the PR. This is only relevant if a PR is changing this workflow.
 #
-# See <https://github.com/actions/labeler/issues/121> for more details.
+# See https://github.com/actions/labeler?tab=readme-ov-file#recommended-permissions for more details.
 
 name: Kani Extra
 on:

docs/src/rust-feature-support.md

@@ -153,18 +153,11 @@ The semantics around some advanced features (traits, types, etc.) from Rust are
 not formally defined which makes it harder to ensure that we can properly model
 all their use cases.
 
-In particular, there are some outstanding issues to note here:
- * Sanity check `Variant` type in projections
-   [#448](https://github.com/model-checking/kani/issues/448).
- * Unexpected fat pointer results in
-   [#277](https://github.com/model-checking/kani/issues/277),
-   [#327](https://github.com/model-checking/kani/issues/327) and
-   [#676](https://github.com/model-checking/kani/issues/676).
-
-We are particularly interested in bug reports concerning
-these features, so please [file a bug
-report](https://github.com/model-checking/kani/issues/new?assignees=&labels=bug&template=bug_report.md)
-if you're aware of one.
+We are aware of a lack of sanity checking the `Variant` type in projections
+[#448](https://github.com/model-checking/kani/issues/448).
+If you become aware of other issues concerning
+these features, please [file a bug
+report](https://github.com/model-checking/kani/issues/new?assignees=&labels=bug&template=bug_report.md).
 
 ### Panic strategies
 

docs/src/rust-feature-support/intrinsics.md

@@ -156,7 +156,7 @@ fabsf32 | Yes | |
 fabsf64 | Yes | |
 fadd_fast | Yes | |
 fdiv_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) |
-float_to_int_unchecked | Partial | [#3629](https://github.com/model-checking/kani/issues/3629) |
+float_to_int_unchecked | Yes | |
 floorf32 | Yes | |
 floorf64 | Yes | |
 fmaf32 | Partial | Results are overapproximated |

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

@@ -70,7 +70,6 @@ impl GotocCtx<'_> {
         } else if self.is_cffi_enabled() && instance.fn_abi().unwrap().conv == CallConvention::C {
             // When C-FFI feature is enabled, we just trust the rust declaration.
             // TODO: Add proper casting and clashing definitions check.
-            // https://github.com/model-checking/kani/issues/1350
             // https://github.com/model-checking/kani/issues/2426
             self.ensure(mangled_fn_name, |gcx, _| {
                 let typ = gcx.codegen_ffi_type(instance);

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

@@ -176,13 +176,6 @@ impl ProjectedPlace {
                 "Unexpected type mismatch in projection:\n{goto_expr:?}\nExpr type\n{expr_ty:?}\nType from MIR\n{ty_from_mir:?}"
             );
             warn!("{}", msg);
-            // TODO: there's an expr type mismatch with the rust 2022-11-20 toolchain
-            // for simd:
-            // https://github.com/model-checking/kani/issues/1926
-            // Disabling it for this specific case.
-            if !(expr_ty.is_integer() && ty_from_mir.is_struct_tag()) {
-                debug_assert!(false, "{}", msg);
-            }
             return Err(Box::new(UnimplementedData::new(
                 "Projection mismatch",
                 "https://github.com/model-checking/kani/issues/277",

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

@@ -522,13 +522,6 @@ impl GotocCtx<'_> {
                         // The only argument should be a self reference
                         let args = vec![place_ref];
 
-                        // We have a known issue where nested Arc and Mutex objects result in
-                        // drop_in_place call implementations that fail to typecheck. Skipping
-                        // drop entirely causes unsound verification results in common cases
-                        // like vector extend, so for now, add a sound special case workaround
-                        // for calls that fail the typecheck.
-                        // https://github.com/model-checking/kani/issues/426
-                        // Unblocks: https://github.com/model-checking/kani/issues/435
                         func.call(args).as_stmt(loc)
                     }
                 }

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

@@ -464,11 +464,6 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Gives the vtable name for a type.
     /// In some cases, we have &T, in other cases T, so normalize.
-    ///
-    /// TODO: to handle trait upcasting, this will need to use a
-    /// poly existential trait type as a part of the key as well.
-    /// See compiler/rustc_middle/src/ty/vtable.rs
-    /// <https://github.com/model-checking/kani/issues/358>
     pub fn vtable_name(&self, t: Ty<'tcx>) -> String {
         format!("{}::vtable", self.normalized_trait_name(t))
     }

library/kani_core/src/mem.rs

@@ -61,9 +61,6 @@ macro_rules! kani_mem {
         /// and 3,
         /// and the value stored must respect the validity invariants for type `T`.
         ///
-        /// TODO: Kani should automatically add those checks when a de-reference happens.
-        /// <https://github.com/model-checking/kani/issues/2975>
-        ///
         /// This function will panic today if the pointer is not null, and it points to an unallocated or
         /// deallocated memory location. This is an existing Kani limitation.
         /// See <https://github.com/model-checking/kani/issues/2690> for more details.