Support passing function pointers as arguments in rcgen
Can be tested by adding the following code to misc.c
:
/** Testing the thread-safety of thread_safe alloc */
// RefinedC does not have forking built-in at the moment, so we axiomatize it using the following [fork] function
typedef void (*fork_fun)(void *);
/* [[rc::parameters("ty : type", "P : {iProp Σ}")]] */
/* [[rc::args("function_ptr<{fn(∀ () : (); &own ty; P) → ∃ () : (), void; True}>", "&own<ty>")]] */
/* [[rc::requires("[P]")]] */
void fork(fork_fun fn, void *arg);
/* [[rc::args("&own<int<size_t>>")]] */
/* [[rc::requires("[initialized \"lock\" lid]", "[initialized \"data\" lid]")]] */
void test_thread_safe_alloc_fork_fn(void *num) {
size_t *num_int = num;
thread_safe_alloc(*num_int);
}
size_t param;
/* [[rc::requires("[initialized \"lock\" lid]", "[initialized \"data\" lid]")]] */
void test_thread_safe_alloc() {
param = 10;
fork(test_thread_safe_alloc_fork_fn, ¶m);
thread_safe_alloc(10);
}