Skip to content

Commit

Permalink
CN: fix the failing memcpy test
Browse files Browse the repository at this point in the history
It turns out the issue was trivial and obvious.
  • Loading branch information
talsewell committed Aug 16, 2023
1 parent 3c267c1 commit b1f9e61
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 0 deletions.
20 changes: 20 additions & 0 deletions tests/cn/get_from_arr.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@

/* originally made by minimising a problematic case from memcpy.c */


char
get_from_arr (char *in_arr)
/*@ requires take IA = each (integer j; 0 <= j && j < 10)
{Owned<char>(in_arr + (j * sizeof<char>))} @*/
/*@ ensures take IA2 = each (integer j; 0 <= j && j < 10)
{Owned<char>(in_arr + (j * sizeof<char>))} @*/
{
char c;

/*@ extract Owned<char>, 4; @*/
/*@ instantiate good<char>, 4; @*/
c = in_arr[4];

return c;
}

1 change: 1 addition & 0 deletions tests/cn/memcpy.c
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ naive_memcpy (char *in_arr, char *out_arr, int i)
/*@ inv {out_arr} unchanged @*/
{
/*@ extract Owned<char>, j; @*/
/*@ instantiate good<char>, j; @*/
out_arr[j] = in_arr[j];
}

Expand Down

0 comments on commit b1f9e61

Please sign in to comment.