mkm: match Rust Option type naming

GaloisInc · Jan 3, 2025 · aa65423 · aa65423
1 parent 59e7337
commit aa65423
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/components/include/cn_memory.h b/components/include/cn_memory.h
@@ -72,12 +72,12 @@ ensures
 /*$
 datatype OptionMemory {
     SomeMemory {{u64 base, u64 size} al, map<u64, u8> bu}, 
-    NothingMemory {}
+    NoneMemory {}
 }
 predicate (datatype OptionMemory) MallocResult(pointer p, u64 n)
 {
   if (is_null(p)) {
-    return NothingMemory {}; 
+    return NoneMemory {}; 
   } else {
     take log = Alloc(p);
     assert(allocs[(alloc_id)p] == log);

diff --git a/components/mission_key_management/client.c b/components/mission_key_management/client.c
@@ -80,24 +80,24 @@ requires ValidState( state );
 /*$ 
 datatype OptionClientObject {
     SomeClientObject {struct client obj}, 
-    NothingClientObject {}
+    NoneClientObject {}
 }
-predicate (OptionClientObject) MaybeClientNew(pointer p, i32 fd, i32 state)
+predicate (OptionClientObject) OptionClientNew(pointer p, i32 fd, i32 state)
 {
     if (is_null(p)) {
-        return NothingClientObject {}; 
+        return NoneClientObject {}; 
     } else {
         take Client_out = ClientObject(p);
         assert(Client_out.fd == fd); 
         assert(((i32) Client_out.state) == state); 
-        return SomeClientObject { obj: Client_out} ;  
+        return SomeClientObject { obj: Client_out } ;  
     }
 }
 $*/
 
 struct client* client_new(int fd) 
 /*$ 
-ensures take Client_out = MaybeClientNew(return, fd, CS_RECV_KEY_ID);
+ensures take Client_out = OptionClientNew(return, fd, CS_RECV_KEY_ID);
 $*/
 {
     struct client* c = malloc(sizeof(struct client));