Skip to content

Commit

Permalink
CN: explicit split_case in funptr tests
Browse files Browse the repository at this point in the history
It works. It could use a less verbose version.
  • Loading branch information
talsewell committed Jan 30, 2024
1 parent b85da48 commit 4a1fd78
Show file tree
Hide file tree
Showing 3 changed files with 34 additions and 0 deletions.
29 changes: 29 additions & 0 deletions tests/cn/fun_addrs_cn_stmt.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@

int global_x;
void *global_void_ptr;

extern int extern_f (void);

int
g (int x)
{
return 0;
}

/*@
function ({u32 x1, u32 x2}) get_globals ()
{ {x1: (u32) (&g), x2: (u32) (&extern_f)} }
@*/

int
f (int x)
/*@ accesses global_x @*/
{
/* resolution of the 'g' & 'extern_f' addrs triggered a bug at one point */
/*@ assert (((u32) (&x)) == ((u32) (&x))); @*/;
/*@ assert (((u32) (&global_x)) == ((u32) (&global_x))); @*/;
/*@ assert (get_globals () == get_globals ()); @*/;
/*@ assert (((u32) (&g)) == ((u32) (&g))); @*/;

return x == global_x;
}
2 changes: 2 additions & 0 deletions tests/cn/fun_ptr_extern.c
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,8 @@ call_site (int x, int y) {
int z;

g2 = get_int_binop(y);
/*@ split_case (ptr_eq (g2, &f1)) @*/;
/*@ split_case (ptr_eq (g2, &f2)) @*/;
z = g2 (x, y);

return z;
Expand Down
3 changes: 3 additions & 0 deletions tests/cn/fun_ptr_three_opts.c
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,9 @@ call_site (int x, int y) {
int z;

g2 = get_int_binop(y);
/*@ split_case (ptr_eq (g2, &f1)); @*/;
/*@ split_case (ptr_eq (g2, &f2)); @*/;
/*@ split_case (ptr_eq (g2, &f3)); @*/;
z = g2 (x, y);

return z;
Expand Down

0 comments on commit 4a1fd78

Please sign in to comment.