Skip to content

Commit

Permalink
CN: add some tests that didn't get committed before
Browse files Browse the repository at this point in the history
  • Loading branch information
talsewell committed Aug 16, 2023
1 parent 9270fcf commit f8bf6fe
Show file tree
Hide file tree
Showing 3 changed files with 47 additions and 0 deletions.
10 changes: 10 additions & 0 deletions tests/cn/left_shift_const.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@

#define BIT(n) (1UL << (n))

int
f (int x) {
int mask = BIT(12 - 3) - 1;

return 0;
}

15 changes: 15 additions & 0 deletions tests/cn/missing_resource.error.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@

/* this is a wrong specification. */
/* this function doesn't create an integer in memory */

int
f (int *p, int x)
/*@ requires x < 12 @*/
/*@ ensures return < 12 @*/
/*@ ensures take Resource_From_Nothing = Owned(p) @*/
{
return x;
}



22 changes: 22 additions & 0 deletions tests/cn/missing_resource_indirect.error.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@

/* this is a wrong specification. */
/* this function doesn't create an integer in memory */

/*@
predicate (integer) Owned_Wrapper (pointer p) {
take I = Owned<int>(p);
return I;
}
@*/

int
f (int *p, int x)
/*@ requires x < 12 @*/
/*@ ensures return < 12 @*/
/*@ ensures take Resource_From_Nothing = Owned_Wrapper(p) @*/
{
return x;
}



0 comments on commit f8bf6fe

Please sign in to comment.