From 928377c60977658bad58b2cabe6af23cc2c5ea68 Mon Sep 17 00:00:00 2001 From: evans1629 Date: Wed, 4 Dec 2002 14:29:21 +0000 Subject: [PATCH] Fixed but with multiple globals clauses reported by Gayath Ratnayaka. --- lib/ansi.h | 227 ++++++++++++++++++++++++++++++++++++++++-------- src/globSet.c | 4 +- src/uentry.c | 8 +- test/modifies.c | 3 +- 4 files changed, 200 insertions(+), 42 deletions(-) diff --git a/lib/ansi.h b/lib/ansi.h index 2274eab..6623d8b 100644 --- a/lib/ansi.h +++ b/lib/ansi.h @@ -1,5 +1,5 @@ /* -** satndard.h --- ISO C99 Standard Library for Splint. +** standard.h --- ISO C99 Standard Library for Splint. ** ** Process with -DSTRICT to get strict library. */ @@ -196,41 +196,167 @@ struct lconv *localeconv (void) /*@*/ ; /* ** math.h +** +** evans 2002-07-03: updated from ISO C99 (http://www.vmunix.com/~gabor/c/draft.html) */ +typedef float float_t; +typedef double double_t; + /*@constant double HUGE_VAL; @*/ +/*@constant float HUGE_VALF; @*/ +/*@constant long double HUGE_VALL; @*/ + +/*@constant float INFINITY; @*/ + +/*@constant float NAN; @*/ + /*:warn implementationoptional "NAN is defined if and only if the implementation supports quiet float type NaNs.":*/ ; + +/*@constant int FP_INFINITE;@*/ +/*@constant int FP_NAN;@*/ +/*@constant int FP_NORMAL;@*/ +/*@constant int FP_SUBNORMAL;@*/ +/*@constant int FP_ZERO;@*/ + +/*@constant int FP_ILOGB0;@*/ +/*@constant int FP_ILOGBNAN;@*/ + +/*@constant int DECIMAL_DIG;@*/ + +/* Defined for specs only - this type is any real type */ +typedef float /*@alt double, long double@*/ s_real_t; + +int fpclassify (/*@sef@*/ s_real_t) /*@*/ ; +int signbit (/*@sef@*/ s_real_t) /*@*/ ; +int isfinite (/*@sef@*/ s_real_t) /*@*/ ; +int isnormal (/*@sef@*/ s_real_t) /*@*/ ; +int isnan (/*@sef@*/ s_real_t) /*@*/ ; +int isinf (/*@sef@*/ s_real_t) /*@*/ ; /* -** math functions that may have a range error modify errno +** math functions that may have a range error modify errno (implementation defined). */ -double sin (double x) /*@*/ ; -double cos (double x) /*@*/ ; -double tan (double x) /*@*/ ; -double asin (double x) /*@modifies errno@*/ ; double acos (double x) /*@modifies errno@*/ ; +double asin (double x) /*@modifies errno@*/ ; double atan (double x) /*@*/ ; double atan2 (double y, double x) /*@*/ ; -double sinh (double x) /*@*/ ; + +double cos (double x) /*@*/ ; +double sin (double x) /*@*/ ; +double tan (double x) /*@*/ ; + double cosh (double x) /*@modifies errno@*/ ; +double sinh (double x) /*@modifies errno@*/ ; double tanh (double x) /*@*/ ; +double acosh (double x) /*@modifies errno@*/ ; +double asinh (double x) /*@modifies errno@*/ ; +double atanh (double x) /*@modifies errno@*/ ; + double exp (double x) /*@modifies errno@*/ ; -double ldexp (double x, int n) /*@modifies errno@*/ ; double frexp (double x, /*@out@*/ int *xp) /*@modifies *xp;@*/ ; +double ldexp (double x, int n) /*@modifies errno@*/ ; double log (double x) /*@modifies errno@*/ ; double log10 (double x) /*@modifies errno@*/ ; +double modf (double x, /*@out@*/ double *ip) /*@modifies *ip;@*/ ; + +double exp2 (double x) /*@modifies errno@*/ ; +double expm1 (double x) /*@modifies errno@*/ ; +double log1p (double x) /*@modifies errno@*/ ; +double log2 (double x) /*@modifies errno@*/ ; +double logb (double x) /*@modifies errno@*/ ; + +double scalbn (double x, int n) /*@modifies errno@*/ ; +double scalbln (double x, long int n) /*@modifies errno@*/ ; +long double scalblnl(long double x, long int n) /*@modifies errno@*/ ; + +int ilogb (double x) /*@modifies errno@*/ ; +int ilogbf (float x) /*@modifies errno@*/ ; +int ilogbl (long double x) /*@modifies errno@*/ ; + +double fabs (double x) /*@*/ ; +float fabsf (float x) /*@*/ ; +long double fabsl (long double x) /*@*/ ; + double pow (double x, double y) /*@modifies errno@*/ ; +float powf(float x, float y) /*@modifies errno@*/ ; +long double powl(long double x, long double y) /*@modifies errno@*/ ; + double sqrt (double x) /*@modifies errno@*/ ; +float sqrtf(float x) /*@modifies errno@*/ ; +long double sqrtl (long double x) /*@modifies errno@*/ ; + +double cbrt (double x) /*@*/ ; +float cbrtf (float x) /*@*/ ; +long double cbrtl (long double x) /*@*/ ; + +double hypot (double x, double y) /*@modifies errno@*/ ; +float hypotf (float x, float y) /*@modifies errno@*/ ; +long double hypotl (long double x, long double y) /*@modifies errno@*/ ; + +double erf (double x) /*@*/ ; +double erfc (double x) /*@*/ ; +float erff (float x) /*@*/ ; +long double erfl (long double x) /*@*/ ; +float erfcf (float x) /*@*/ ; +long double erfcl (long double x) /*@*/ ; + +double gamma (double x) /*@modifies errno@*/ ; +float gammaf(float x) /*@modifies errno@*/ ; +long double gammal (long double x) /*@modifies errno@*/ ; +double lgamma (double x) /*@modifies errno@*/ ; +float lgammaf (float x) /*@modifies errno@*/ ; +long double lgammal (long double x) /*@modifies errno@*/ ; double ceil (double x) /*@*/ ; +float ceilf(float x) /*@*/ ; +long double ceill(long double x) /*@*/ ; + double floor (double x) /*@*/ ; -double fabs (double x) /*@*/ ; +float floorf (float x) /*@*/ ; +long double floorl (long double x) /*@*/ ; -double modf (double x, /*@out@*/ double *ip) /*@modifies *ip;@*/ ; +double nearbyint (double x) /*@*/ ; +float nearbyintf (float x) /*@*/ ; +long double nearbyintl (long double x) /*@*/ ; + +double rint (double x) /*@*/; +float rintf (float x) /*@*/ ; +long double rintl (long double x) /*@*/ ; +long int lrint (double x) /*@modifies errno@*/ ; +long int lrintf (float x) /*@modifies errno@*/ ; +long int lrintl (long double x) /*@modifies errno@*/ ; +long long llrint (double x) /*@modifies errno@*/ ; +long long llrintf(float x) /*@modifies errno@*/ ; +long long llrintl(long double x) /*@modifies errno@*/ ; + +double round (double x) /*@*/ ; +long int lround (double x) /*@modifies errno@*/ ; +long long llround (double x) /*@modifies errno@*/ ; + +double trunc (double x) /*@*/ ; double fmod (double x, double y) /*@*/ ; +double remainder (double x, double y) /*@*/ ; +double remquo (double x, double y, /*@out@*/ int *quo) /*@modifies *quo@*/ ; +double copysign (double x, double y) /*@*/ ; +double nan (/*@nullterminated@*/ const char *tagp) /*@*/ ; +double nextafter (double x, double y) /*@*/ ; +double nextafterx (double x, long double y) /*@*/ ; + +double fdim (double x, double y) /*@modifies errno@*/ ; +double fmax (double x, double y) /*@*/ ; +double fmin (double x, double y) /*@*/ ; +double fma (double x, double y, double z) /*@*/ ; + +int isgreater (s_real_t x, s_real_t y) /*@*/ ; +int isgreaterequal (s_real_t x, s_real_t y) /*@*/ ; +int isless (s_real_t x, s_real_t y) /*@*/ ; +int islessequal (s_real_t x, s_real_t y) /*@*/ ; +int islessgreater (s_real_t x, s_real_t y) /*@*/ ; +int isunordered (s_real_t x, s_real_t y) /*@*/ ; /* ** These functions are optional in iso C. An implementation does not @@ -343,11 +469,12 @@ void va_end (va_list va) /*@modifies va;@*/ ; typedef /*@abstract@*/ /*@mutable@*/ void *FILE; typedef /*@abstract@*/ /*@mutable@*/ void *fpos_t; -/*@constant int _IOFBF; @*/ -/*@constant int _IOLBF; @*/ -/*@constant int _IONBF; @*/ +/*@constant size_t _IOFBF; @*/ +/*@constant size_t _IOLBF; @*/ +/*@constant size_t _IONBF; @*/ + +/*@constant size_t BUFSIZ; @*/ /* evans 2002-02-27 change suggested by Walter Briscoe */ -/*@constant int BUFSIZ; @*/ /*@constant int EOF; @*/ /*@constant int FOPEN_MAX; @*/ @@ -374,27 +501,34 @@ typedef /*@abstract@*/ /*@mutable@*/ void *fpos_t; int remove (char *filename) /*@modifies fileSystem, errno@*/ ; int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ; -/*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem@*/ ; +/*@dependent@*/ /*@null@*/ FILE *tmpfile (void) + /*@modifies fileSystem, errno@*/ ; + /*@observer@*/ char * tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s) /*@modifies *s, internalState@*/ ; -int fclose (FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ; +int fclose (FILE *stream) + /*@modifies *stream, errno, fileSystem;@*/ ; + int fflush (/*@null@*/ FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ; /*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode) /*@modifies fileSystem@*/ ; -/*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream) +/*@dependent@*/ /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream) /*@modifies *stream, fileSystem, errno@*/ ; - extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf) - /*@modifies fileSystem, *stream, *buf@*/ ; +void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf) + /*@modifies fileSystem, *stream, *buf@*/ + /*:errorcode != 0*/ ; + /*:requires maxSet(buf) >= (BUFSIZ - 1):*/ ; - extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf, - int mode, size_t size) - /*@modifies fileSystem, *stream, *buf@*/ ; +int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf, + int mode, size_t size) + /*@modifies fileSystem, *stream, *buf@*/ + /*@requires maxSet(buf) >= (size - 1) @*/ ; # ifdef STRICT /*@printflike@*/ @@ -408,7 +542,7 @@ int /*@alt void@*/ fprintf (FILE *stream, char *format, ...) /*@scanflike@*/ int fscanf (FILE *stream, char *format, ...) - /*@modifies fileSystem, *stream@*/ ; + /*@modifies fileSystem, *stream, errno@*/ ; # ifdef STRICT /*@printflike@*/ @@ -425,20 +559,29 @@ int /*@alt void@*/ printf (char *format, ...) /*@scanflike@*/ int scanf(char *format, ...) /*@globals stdin@*/ - /*@modifies fileSystem, *stdin@*/ ; + /*@modifies fileSystem, *stdin, errno@*/ ; + /*drl added errno 09-19-2001 */ ; # ifdef STRICT /*@printflike@*/ int sprintf (/*@out@*/ char *s, char *format, ...) + /*@warn bufferoverflowhigh "Buffer overflow possible with sprintf. Recommend using snprintf instead"@*/ /*@modifies *s@*/ ; # else /*@printflike@*/ int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...) + /*@warn bufferoverflowhigh "Buffer overflow possible with sprintf. Recommend using snprintf instead"@*/ /*@modifies *s@*/ ; # endif +/* evans 2002-07-09: snprintf added to standard.h (from unix.h) */ +/*@printflike@*/ +int snprintf (/*@out@*/ char * restrict s, size_t n, const char * restrict format, ...) + /*@modifies s@*/ + /*@requires maxSet(s) >= (n - 1)@*/ ; + /*@scanflike@*/ -int sscanf (/*@out@*/ char *s, char *format, ...) /*@*/ ; +int sscanf (/*@out@*/ char *s, char *format, ...) /*@modifies errno@*/ ; /* modifies extra arguments */ int vprintf (const char *format, va_list arg) @@ -453,7 +596,7 @@ int vsprintf (/*@out@*/ char *str, const char *format, va_list ap) /*@modifies str@*/ ; int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap) - /*@requires maxSet(str) >= size@*/ + /*@requires maxSet(str) >= (size - 1)@*/ /* drl - this was size, size-1 in stdio.h */ /*@modifies str@*/ ; int fgetc (FILE *stream) @@ -475,9 +618,9 @@ int fputs (char *s, FILE *stream) /* note use of sef --- stream may be evaluated more than once */ int getc (/*@sef@*/ FILE *stream) - /*@modifies fileSystem, *stream@*/ ; + /*@modifies fileSystem, *stream, errno@*/ ; -int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ; +int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin, errno@*/ ; /*@null@*/ char *gets (/*@out@*/ char *s) /*@warn bufferoverflowhigh @@ -486,29 +629,36 @@ int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ; int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream) /*:errorcode EOF:*/ - /*@modifies fileSystem, *stream;@*/ ; + /*@modifies fileSystem, *stream, errno;@*/ ; int putchar (int /*@alt char@*/ c) /*:errorcode EOF:*/ - /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ; + /*@globals stdout@*/ + /*@modifies fileSystem, *stdout, errno@*/ ; int puts (const char *s) /*:errorcode EOF:*/ /*@globals stdout@*/ - /*@modifies fileSystem, *stdout@*/ ; + /*@modifies fileSystem, *stdout, errno@*/ ; int ungetc (int /*@alt char@*/ c, FILE *stream) - /*@modifies fileSystem, *stream, errno@*/ ; + /*@modifies fileSystem, *stream@*/ ; + /*drl REMOVED errno 09-19-2001*/ size_t fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream) - /*@modifies fileSystem, *ptr, *stream, errno@*/ ; + /*@modifies fileSystem, *ptr, *stream, errno@*/ + /*requires maxSet(ptr) >= (size - 1) @*/ + /*@ensures maxRead(ptr) == (size - 1) @*/ ; size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream) - /*@modifies fileSystem, *stream, errno@*/ ; + /*@modifies fileSystem, *stream, errno@*/ + /*@requires maxRead(ptr) >= size @*/ ; int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos) - /*@modifies *pos, errno@*/ ; + /*@modifies *pos, errno@*/ + /*@requires maxSet(pos) >= 0@*/ + /*@ensures maxRead(pos) >= 0 @*/; int fseek (FILE *stream, long int offset, int whence) /*:errorcode -1:*/ @@ -524,6 +674,7 @@ void rewind (FILE *stream) /*@modifies *stream@*/ ; void clearerr (FILE *stream) /*@modifies *stream@*/ ; int feof (FILE *stream) /*@modifies errno@*/ ; + int ferror (FILE *stream) /*@modifies errno@*/ ; void perror (/*@null@*/ char *s) @@ -880,7 +1031,9 @@ void /*@alt char * @*/ void /*@alt char * @*/ strncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2, size_t n) - /*@modifies *s1@*/ /*@requires maxSet(s1) >= ( n - 1 ); @*/ /*@ensures maxRead (s2) >= maxRead(s1) /\ maxRead (s1) <= n; @*/; + /*@modifies *s1@*/ + /*@requires maxSet(s1) >= ( n - 1 ); @*/ + /*@ensures maxRead (s2) >= maxRead(s1) /\ maxRead (s1) <= n; @*/ ; void /*@alt char * @*/ strcat (/*@unique@*/ /*@returned@*/ char *s1, char *s2) @@ -927,7 +1080,7 @@ size_t strcspn (char *s1, char *s2) /*@*/ ; size_t strspn (char *s, char *t) /*@*/ ; /*@null@*/ /*@exposed@*/ char * - strstr (/*@returned@*/ /*@unique@*/ char *s, char *t) /*@*/ + strstr (/*@returned@*/ const char *s, const char *t) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 /\ maxRead(result) >= maxRead(t) /\ maxSet(result) >= maxRead(t)@*/ ; /*@null@*/ /*@exposed@*/ char * diff --git a/src/globSet.c b/src/globSet.c index d3b1958..f4142b8 100644 --- a/src/globSet.c +++ b/src/globSet.c @@ -167,8 +167,8 @@ globSet_undump (char **s) /*@only@*/ cstring globSet_unparse (globSet ll) { - return (sRefSet_unparseFull (ll)); - /* return (sRefSet_unparsePlain (ll)); */ + /* return (sRefSet_unparseFull (ll)); */ + return (sRefSet_unparsePlain (ll)); } int diff --git a/src/uentry.c b/src/uentry.c index 666eb9c..9e59baf 100644 --- a/src/uentry.c +++ b/src/uentry.c @@ -1057,14 +1057,18 @@ static void uentry_reflectClauses (uentry ue, functionClauseList clauses) if (uentry_hasGlobs (ue)) { - voptgenerror + vgenhinterror (FLG_SYNTAX, message ("Multiple globals clauses for %q: %q", uentry_getName (ue), globalsClause_unparse (glc)), + cstring_makeLiteral ("Only one globals clause may be used. The second globals clause is ignored."), globalsClause_getLoc (glc)); - uentry_setGlobals (ue, globalsClause_takeGlobs (glc)); /*@i32@*/ + + /* + uentry_setGlobals (ue, globalsClause_takeGlobs (glc)); + */ } else { diff --git a/test/modifies.c b/test/modifies.c index 854d01d..898ed97 100644 --- a/test/modifies.c +++ b/test/modifies.c @@ -4,7 +4,8 @@ static int mstat; static /*@unused@*/ int internalState; int f3 (int p[]) - /*@modifies internalState, fileSystem;@*/ ; /* 1. Modifies list uses ... */ + /*@modifies + internalState, fileSystem;@*/ ; /* 1. Modifies list uses ... */ int f4 (int p[]) /*@modifies p[3];@*/; -- 2.45.2