diff options
| author | jbj <devnull@localhost> | 2002-07-03 14:01:49 +0000 |
|---|---|---|
| committer | jbj <devnull@localhost> | 2002-07-03 14:01:49 +0000 |
| commit | af3c677f06687e5ad1e33eb24f984c7ac5ff2a33 (patch) | |
| tree | 9f18227a31e49ecccafa3852610d3346594dad69 /rpmio | |
| parent | e5fb770e7d9aac53a513965c0f2bcf360934794b (diff) | |
| download | rpm-af3c677f06687e5ad1e33eb24f984c7ac5ff2a33.tar.gz rpm-af3c677f06687e5ad1e33eb24f984c7ac5ff2a33.tar.bz2 rpm-af3c677f06687e5ad1e33eb24f984c7ac5ff2a33.zip | |
- use rpmfi in showQueryPackage(), eliminating headerGetEntry().
CVS patchset: 5538
CVS date: 2002/07/03 14:01:49
Diffstat (limited to 'rpmio')
| -rw-r--r-- | rpmio/rpmio.h | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/rpmio/rpmio.h b/rpmio/rpmio.h index bb028c483..a05e2a50f 100644 --- a/rpmio/rpmio.h +++ b/rpmio/rpmio.h @@ -61,7 +61,7 @@ typedef ssize_t (*fdio_read_function_t) (void *cookie, char *buf, size_t nbytes) /*@globals errno, fileSystem @*/ /*@modifies *cookie, errno, fileSystem @*/ /*@requires maxSet(buf) >= (nbytes - 1) @*/ - /*@ensures maxRead(buf) >= nbytes @*/ ; + /*@ensures maxRead(buf) == result @*/ ; /** */ @@ -235,16 +235,23 @@ struct FDIO_s { /** * fread(3) clone. */ +/*@-incondefs@*/ size_t Fread(/*@out@*/ void * buf, size_t size, size_t nmemb, FD_t fd) /*@globals fileSystem @*/ - /*@modifies fd, *buf, fileSystem @*/; + /*@modifies fd, *buf, fileSystem @*/ + /*@requires maxSet(buf) >= (nmemb - 1) @*/ + /*@ensures maxRead(buf) == result @*/; +/*@=incondefs@*/ /** * fwrite(3) clone. */ +/*@-incondefs@*/ size_t Fwrite(const void * buf, size_t size, size_t nmemb, FD_t fd) /*@globals fileSystem @*/ - /*@modifies fd, fileSystem @*/; + /*@modifies fd, fileSystem @*/ + /*@requires maxRead(buf) >= nmemb @*/; +/*@=incondefs@*/ /** * fseek(3) clone. @@ -360,7 +367,7 @@ int Readlink(const char * path, /*@out@*/ char * buf, size_t bufsiz) /*@globals errno, fileSystem @*/ /*@modifies *buf, errno, fileSystem @*/ /*@requires maxSet(buf) >= (bufsiz - 1) @*/ - /*@ensures result <= bufsiz @*/; + /*@ensures maxRead(buf) <= bufsiz @*/; /*@=incondefs@*/ /** @@ -474,7 +481,7 @@ ssize_t fdRead(void * cookie, /*@out@*/ char * buf, size_t count) /*@globals errno, fileSystem @*/ /*@modifies *cookie, *buf, errno, fileSystem @*/ /*@requires maxSet(buf) >= (count - 1) @*/ - /*@ensures maxRead(buf) >= count @*/ ; + /*@ensures maxRead(buf) == result @*/ ; #define fdRead(_fd, _buf, _count) fdio->read((_fd), (_buf), (_count)) /*@=incondefs@*/ |