diff options
Diffstat (limited to 'src/alignio.h')
| -rw-r--r-- | src/alignio.h | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/src/alignio.h b/src/alignio.h index 72996b29..be949e26 100644 --- a/src/alignio.h +++ b/src/alignio.h @@ -26,13 +26,14 @@ /*@ @ requires \valid_function(fnct_pread); @ requires \valid(disk_car); + @ requires valid_disk(disk_car); @ requires disk_car->sector_size > 0; @ requires disk_car->offset < 0x8000000000000000; @ requires 0 < count < 0x8000000000000000; @ requires offset < 0x8000000000000000; @ requires \valid((char *)buf + (0 .. count -1)); - @ requires disk_car->rbuffer == \null || (\freeable(disk_car->rbuffer) && disk_car->rbuffer_size > 0); - @ ensures disk_car->rbuffer == \null || (\freeable(disk_car->rbuffer) && disk_car->rbuffer_size > 0); + @ requires \separated(disk_car, (char *)buf); + @ ensures valid_disk(disk_car); @*/ static int align_pread(int (*fnct_pread)(const disk_t *disk_car, void *buf, const unsigned int count, const uint64_t offset), disk_t *disk_car, void*buf, const unsigned int count, const uint64_t offset) @@ -64,13 +65,17 @@ static int align_pread(int (*fnct_pread)(const disk_t *disk_car, void *buf, cons } /*@ assert disk_car->rbuffer_size >= count_new; */ disk_car->rbuffer=(char*)MALLOC(disk_car->rbuffer_size); + /*@ assert valid_disk(disk_car); */ } /*@ assert \freeable(disk_car->rbuffer); */ + /*@ assert valid_disk(disk_car); */ res=fnct_pread(disk_car, disk_car->rbuffer, count_new, offset_new/disk_car->sector_size*disk_car->sector_size); memcpy(buf,(char*)disk_car->rbuffer+(offset_new%disk_car->sector_size),count); /*@ assert \freeable(disk_car->rbuffer) && disk_car->rbuffer_size > 0; */ + /*@ assert valid_disk(disk_car); */ return (res < (signed)count ? res : (signed)count ); } + /*@ assert valid_disk(disk_car); */ return fnct_pread(disk_car, buf, count, offset_new); } @@ -78,13 +83,14 @@ static int align_pread(int (*fnct_pread)(const disk_t *disk_car, void *buf, cons @ requires \valid_function(fnct_pread); @ requires \valid_function(fnct_pwrite); @ requires \valid(disk_car); + @ requires valid_disk(disk_car); @ requires disk_car->sector_size > 0; @ requires disk_car->offset < 0x8000000000000000; @ requires 0 < count < 0x8000000000000000; @ requires offset < 0x8000000000000000; @ requires \valid_read((char *)buf + (0 .. count -1)); - @ requires disk_car->wbuffer == \null || \freeable(disk_car->wbuffer); - @ ensures disk_car->wbuffer == \null || \freeable(disk_car->wbuffer); + @ requires \separated(disk_car, (char *)buf); + @ ensures valid_disk(disk_car); @*/ static int align_pwrite(int (*fnct_pread)(const disk_t *disk_car, void *buf, const unsigned int count, const uint64_t offset), int (*fnct_pwrite)(disk_t *disk_car, const void *buf, const unsigned int count, const uint64_t offset), @@ -113,8 +119,10 @@ static int align_pwrite(int (*fnct_pread)(const disk_t *disk_car, void *buf, con } /*@ assert disk_car->wbuffer_size >= count_new; */ disk_car->wbuffer=(char*)MALLOC(disk_car->wbuffer_size); + /*@ assert valid_disk(disk_car); */ } /*@ assert \freeable(disk_car->wbuffer); */ + /*@ assert valid_disk(disk_car); */ if(fnct_pread(disk_car, disk_car->wbuffer, count_new, offset_new/disk_car->sector_size*disk_car->sector_size)<0) { log_error("read failed but trying to write anyway"); @@ -123,8 +131,10 @@ static int align_pwrite(int (*fnct_pread)(const disk_t *disk_car, void *buf, con memcpy((char*)disk_car->wbuffer+(offset_new%disk_car->sector_size),buf,count); tmp=fnct_pwrite(disk_car, disk_car->wbuffer, count_new, offset_new/disk_car->sector_size*disk_car->sector_size); /*@ assert \freeable(disk_car->wbuffer) && disk_car->wbuffer_size > 0; */ + /*@ assert valid_disk(disk_car); */ return (tmp < (signed)count ? tmp : (signed)count); } + /*@ assert valid_disk(disk_car); */ return fnct_pwrite(disk_car, buf, count, offset_new); } #endif |