Add support for abi

verus-lang · Nov 16, 2023 · ff97974 · ff97974
1 parent 113282d
commit ff97974
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 5 deletions.
diff --git a/examples/wip.rs b/examples/wip.rs
@@ -1,9 +1,11 @@
 verus! {
 
-fn test() {
-    for CKeyKV { k, v } in v {
-        res.insert(k, v);
-    }
+#[verifier(external_body)]
+pub struct NetClientCPointers {
+    get_time_func: extern "C" fn() -> u64,
+    receive_func: extern "C" fn(i32, *mut bool, *mut bool, *mut *mut std::vec::Vec<u8>, *mut *mut std::vec::Vec<u8>),
+    send_func: extern "C" fn(u64, *const u8, u64, *const u8) -> bool
 }
 
+
 } // verus!
diff --git a/src/lib.rs b/src/lib.rs
@@ -637,7 +637,7 @@ fn to_doc<'a>(
                 }
             }))
         }
-        Rule::abi => unsupported(pair),
+        Rule::abi => map_to_doc(ctx, arena, pair).append(arena.text(" ")),
         Rule::param_list => comma_delimited(ctx, arena, pair).parens().group(),
         Rule::closure_param_list => comma_delimited(ctx, arena, pair)
             .enclose(arena.text("|"), arena.text("|"))