Let malloc possibly fail

components/include/cn_memory.h

@@ -56,17 +56,32 @@ ensures
     true;
 $*/
 
+/*$
+datatype newmem {
+NewMemF {{u64 base, u64 size} al, map<u64, u8> bu}
+}
+
+predicate (datatype newmem) MallocResult(pointer p, u64 n)
+{
+  if (is_null(p)) {
+  return NewMemF { al : default<{u64 base, u64 size}>, bu : default<map<u64, u8> >};
+  } else {
+    take log = Alloc(p);
+    assert(allocs[(alloc_id)p] == log);
+    assert(log.base == (u64) p);
+    assert(log.size == n);
+    take i = each(u64 j; j >= 0u64 && j < n) {Block<uint8_t>(array_shift<uint8_t>(p, j))};
+
+    return NewMemF { al : log, bu : i};
+  }
+}
+$*/
 void *_malloc(size_t n);
 /*$
 spec _malloc(u64 n);
 requires true;
 ensures
-    !is_null(return);
-    take log = Alloc(return);
-    allocs[(alloc_id)return] == log;
-    log.base == (u64) return;
-    log.size == n;
-    take i = each(u64 j; j >= 0u64 && j < n) {Block<uint8_t>(array_shift<uint8_t>(return, j))};
+    take out = MallocResult(return, n);
 $*/
 
 #endif // CN_MEMCPY_H_

components/mission_key_management/client.c

@@ -74,14 +74,38 @@ requires ValidState( state );
         } 
     }
 }
+/*$
+datatype newmem_client {
+NewMemClientF {{u64 base, u64 size} al, struct client bu}
+}
 
+predicate (datatype newmem_client) MallocResult_Owned_struct_client(pointer p)
+{
+  if (is_null(p)) {
+    return NewMemClientF { al : default<{u64 base, u64 size}>, bu : default<struct client>};
+  } else {
+    let n = sizeof<struct client>;
+    take log = Alloc(p);
+    assert(allocs[(alloc_id)p] == log);
+    assert(log.base == (u64) p);
+    assert(log.size == n);
+    take i = Owned<struct client>(p);
+
+    return NewMemClientF { al : log, bu : i};
+  }
+}
+$*/
 struct client* client_new(int fd) 
 // TODO: Specification doesn't handle the case where malloc fails 
 /*$ 
-ensures take Client_out = ClientPred(return);
-        take log = Alloc(return);
-        Client_out.fd == fd; 
-        ((i32) Client_out.state) == CS_RECV_KEY_ID;
+ensures
+    take nmem = MallocResult_Owned_struct_client(return);
+    let Client_out = match nmem {
+      NewMemClientF {al: _, bu: x} => {x}
+    };
+    is_null(return) ? true : Client_out.fd == fd;
+    is_null(return) ? true : Client_out.pos == 0u8;
+    is_null(return) ? true : ((i32) Client_out.state) == CS_RECV_KEY_ID;
 $*/
 {
     struct client* c = malloc(sizeof(struct client));