remove/update KANI_TODO

src/lib/twizzler-abi/src/object.rs

@@ -1,9 +1,5 @@
 //! Low-level object APIs, mostly around IDs and basic things like protection definitions and metadata.
 
-/*
-KANI_TODO
-*/
-
 use core::fmt::{LowerHex, UpperHex};
 /// The maximum size of an object, including null page and meta page(s).
 pub const MAX_SIZE: usize = 1024 * 1024 * 1024;

src/lib/twizzler-abi/src/runtime/simple_mutex.rs

@@ -6,26 +6,6 @@ use core::{
     sync::atomic::{AtomicU64, Ordering},
 };
 
-/*
-KANI_TODO
-*/
-
-#[cfg(kani)]
-#[kani::proof]
-pub fn it_locks(){
-    // let var:bool = kani::any();
-    // assert!(var | !var);
-
-    let mutex = MutexImp::new();
-    unsafe {
-        mutex.lock();
-    }
-    kani::assert(mutex.is_locked(), "mutex must be locked");
-    unsafe {
-        mutex.unlock();
-    }
-    kani::assert(!mutex.is_locked(), "mutex must not be locked");
-}
 
 
 use crate::syscall::{

src/lib/twizzler-abi/src/thread.rs

@@ -1,8 +1,6 @@
 //! Functions for manipulating threads.
 
-/*
-KANI_TODO
-*/
+
 
 use core::sync::atomic::{AtomicU64, Ordering};
 #[cfg(not(feature = "kernel"))]
@@ -79,6 +77,13 @@ impl ExecutionState {
 }
 
 
+
+/*
+KANI_TODO: 
+- Explore more thread behavior/states
+- Finish syscall stub
+*/
+
 #[cfg(kani)]
 mod thread_verif{
     use super::ExecutionState;
@@ -109,6 +114,7 @@ mod thread_verif{
 
     }
 
+    #[cfg(kani)]
     #[kani::proof]
     #[kani::stub(crate::arch::syscall::raw_syscall, stub_raw_syscall)]
     pub fn fixme_thread_set_state(){