From 009ba6e3452df29cbf1757bc0c79dc14683a98da Mon Sep 17 00:00:00 2001 From: "Eric S. Raymond" Date: Sat, 28 Mar 2015 19:02:23 -0400 Subject: Clean up most spint errors. All regression tests pass. --- SConstruct | 2 +- bits.c | 6 +++--- driver_evermore.c | 6 +++--- driver_nmea2000.c | 24 ++++++++++++------------ driver_superstar2.c | 4 ++-- gpsctl.c | 2 +- gpsmon.c | 8 +++++--- gpspipe.c | 6 ++++-- gpsutils.c | 17 +++++++++++++---- libgps_shm.c | 2 +- libgpsd_core.c | 8 ++++---- serial.c | 6 ++---- 12 files changed, 51 insertions(+), 40 deletions(-) diff --git a/SConstruct b/SConstruct index 5c9d8eb6..3da87994 100644 --- a/SConstruct +++ b/SConstruct @@ -1439,7 +1439,7 @@ def Utility(target, source, action): # Note: test_bits.c is unsplintable because of the PRI64 macros. # If you get preprocessor or fatal errors, add +showscan. # explicitly force splint to only use our splintrc file -splintopts = "-I/usr/include/libusb-1.0 +quiet +nof -f .splintrc" +splintopts = "-I/usr/include/libusb-1.0 +quiet +nof +showscan -f .splintrc" if sys.platform.startswith('darwin'): splintopts = splintopts + " +skip-sys-headers" diff --git a/bits.c b/bits.c index bba72e46..cae3db17 100644 --- a/bits.c +++ b/bits.c @@ -25,16 +25,16 @@ uint64_t ubits(unsigned char buf[], unsigned int start, unsigned int width, bool unsigned int i; unsigned end; - assert(width <= sizeof(uint64_t) * CHAR_BIT); + /*@i1@*/ assert(width <= sizeof(uint64_t) * CHAR_BIT); for (i = start / CHAR_BIT; i < (start + width + CHAR_BIT - 1) / CHAR_BIT; i++) { - fld <<= CHAR_BIT; + /*@i1@*/ fld <<= CHAR_BIT; fld |= (unsigned char)buf[i]; } end = (start + width) % CHAR_BIT; if (end != 0) { - fld >>= (CHAR_BIT - end); + /*@i1@*/ fld >>= (CHAR_BIT - end); } /*@ -shiftimplementation @*/ diff --git a/driver_evermore.c b/driver_evermore.c index 0a26ff96..38d4eeaf 100644 --- a/driver_evermore.c +++ b/driver_evermore.c @@ -462,7 +462,7 @@ static bool evermore_protocol(struct gps_device_t *session, int protocol) /*@ -charint @*/ gpsd_log(&session->context->errout, LOG_PROG, "evermore_protocol(%d)\n", protocol); - tmp8 = (protocol != 0) ? 1 : 0; + /*@i1@*/ tmp8 = (protocol != 0) ? 1 : 0; /* NMEA : binary */ evrm_protocol_config[1] = tmp8; return (evermore_control_send @@ -493,10 +493,10 @@ static bool evermore_nmea_config(struct gps_device_t *session, int mode) /*@ -charint */ gpsd_log(&session->context->errout, LOG_PROG, "evermore_nmea_config(%d)\n", mode); - tmp8 = (mode == 1) ? 5 : 1; + /*@i1@*/ tmp8 = (mode == 1) ? 5 : 1; /* NMEA GPGSV, gpsd */ evrm_nmeaout_config[6] = tmp8; /* GPGSV, 1s or 5s */ - tmp8 = (mode == 2) ? 1 : 0; + /*@i1@*/ tmp8 = (mode == 2) ? 1 : 0; /* NMEA PEMT101 */ evrm_nmeaout_config[9] = tmp8; /* PEMT101, 1s or 0s */ return (evermore_control_send(session, (char *)evrm_nmeaout_config, diff --git a/driver_nmea2000.c b/driver_nmea2000.c index 0975e4c0..0ede7e79 100644 --- a/driver_nmea2000.c +++ b/driver_nmea2000.c @@ -67,7 +67,7 @@ static int scale_int(int32_t var, const int64_t factor) ret = var; ret *= factor; - ret >>= 32; + /*@i1@*/ ret >>= 32; return((int)ret); } @@ -1395,36 +1395,36 @@ static void find_pgn(struct can_frame *frame, struct gps_device_t *session) gpsd_log(&session->context->errout, LOG_DATA, "pgn %6d:%s \n", work->pgn, work->name); session->driver.nmea2000.workpgn = (void *) work; - session->lexer.outbuflen = frame->can_dlc & 0x0f; + /*@i1@*/session->lexer.outbuflen = frame->can_dlc & 0x0f; for (l2=0;l2lexer.outbuflen;l2++) { - session->lexer.outbuffer[l2]= frame->data[l2]; + /*@i1@*/session->lexer.outbuffer[l2]= frame->data[l2]; } - } else if ((frame->data[0] & 0x1f) == 0) { + /*@i1@*/} else if ((frame->data[0] & 0x1f) == 0) { unsigned int l2; - session->driver.nmea2000.fast_packet_len = frame->data[1]; - session->driver.nmea2000.idx = frame->data[0]; + /*@i2@*/session->driver.nmea2000.fast_packet_len = frame->data[1]; + /*@i2@*/session->driver.nmea2000.idx = frame->data[0]; #if NMEA2000_FAST_DEBUG gpsd_log(&session->context->errout, LOG_ERROR, "Set idx %2x %2x %2x %6d\n", - frame->data[0], + /*@i1@*/frame->data[0], session->driver.nmea2000.unit, - frame->data[1], + /*@i1@*/frame->data[1], source_pgn); #endif /* of #if NMEA2000_FAST_DEBUG */ session->lexer.inbuflen = 0; session->driver.nmea2000.idx += 1; for (l2=2;l2<8;l2++) { - session->lexer.inbuffer[session->lexer.inbuflen++] = frame->data[l2]; + /*@i1@*/session->lexer.inbuffer[session->lexer.inbuflen++] = frame->data[l2]; } gpsd_log(&session->context->errout, LOG_DATA, "pgn %6d:%s \n", work->pgn, work->name); - } else if (frame->data[0] == session->driver.nmea2000.idx) { + /*@i1@*/} else if (frame->data[0] == session->driver.nmea2000.idx) { unsigned int l2; for (l2=1;l2<8;l2++) { if (session->driver.nmea2000.fast_packet_len > session->lexer.inbuflen) { - session->lexer.inbuffer[session->lexer.inbuflen++] = frame->data[l2]; + /*@i1@*/session->lexer.inbuffer[session->lexer.inbuflen++] = frame->data[l2]; } } if (session->lexer.inbuflen == session->driver.nmea2000.fast_packet_len) { @@ -1450,7 +1450,7 @@ static void find_pgn(struct can_frame *frame, struct gps_device_t *session) gpsd_log(&session->context->errout, LOG_ERROR, "Fast error %2x %2x %2x %2x %6d\n", session->driver.nmea2000.idx, - frame->data[0], + /*@i2@*/frame->data[0], session->driver.nmea2000.unit, (unsigned int) session->driver.nmea2000.fast_packet_len, source_pgn); diff --git a/driver_superstar2.c b/driver_superstar2.c index e57463b1..90cdcd28 100644 --- a/driver_superstar2.c +++ b/driver_superstar2.c @@ -115,8 +115,8 @@ superstar2_msg_navsol_lla(struct gps_device_t *session, mask |= LATLON_SET | ALTITUDE_SET | SPEED_SET | TRACK_SET | CLIMB_SET; session->gpsdata.satellites_used = (int)getub(buf, 71) & 0x0f; - session->gpsdata.dop.hdop = getleu16(buf, 66) * 0.1; - session->gpsdata.dop.vdop = getleu16(buf, 68) * 0.1; + /*@i1@*/session->gpsdata.dop.hdop = getleu16(buf, 66) * 0.1; + /*@i1@*/session->gpsdata.dop.vdop = getleu16(buf, 68) * 0.1; /* other DOP if available */ mask |= DOP_SET | USED_IS; diff --git a/gpsctl.c b/gpsctl.c index 0e3cbf2b..4e6c241b 100644 --- a/gpsctl.c +++ b/gpsctl.c @@ -657,7 +657,7 @@ int main(int argc, char **argv) } gpsd_log(&context.errout, LOG_INF, "device %s activated\n", session.gpsdata.dev.path); - FD_SET(session.gpsdata.gps_fd, &all_fds); + /*@i1@*/FD_SET(session.gpsdata.gps_fd, &all_fds); if (session.gpsdata.gps_fd > maxfd) maxfd = session.gpsdata.gps_fd; diff --git a/gpsmon.c b/gpsmon.c index caa79397..59405d53 100644 --- a/gpsmon.c +++ b/gpsmon.c @@ -220,6 +220,7 @@ static void cond_hexdump(/*@out@*/char *buf2, size_t len2, /*@-type -noeffect@*/ /* splint is confused about struct timespec */ void toff_update(WINDOW *win, int y, int x) { + assert(win != NULL); if (time_offset.real.tv_sec != 0) { /* NOTE: can not use double here due to precision requirements */ @@ -258,6 +259,7 @@ void pps_update(WINDOW *win, int y, int x) /*@-type -noeffect@*/ /* splint is confused about struct timespec */ struct timedelta_t ppstimes; + assert(win != NULL); if (pps_thread_ppsout(&session.pps_thread, &ppstimes) > 0) { /* NOTE: can not use double here due to precision requirements */ struct timespec timedelta; @@ -601,7 +603,7 @@ static void select_packet_monitor(struct gps_device_t *device) } /*@+globstate@*/ -/*@-statictrans -globstate@*/ +/*@-statictrans -globstate -unrecog@*/ static /*@null@*/ char *curses_get_command(void) /* char-by-char nonblocking input, return accumulated command line on \n */ { @@ -655,7 +657,7 @@ static /*@null@*/ char *curses_get_command(void) return line; } -/*@+statictrans +globstate@*/ +/*@+statictrans +globstate +unrecog@*/ /****************************************************************************** * @@ -1377,7 +1379,7 @@ int main(int argc, char **argv) (void)tcgetattr(0, &cooked); (void)tcgetattr(0, &rare); rare.c_lflag &=~ (ICANON | ECHO); - rare.c_cc[VMIN] = (cc_t)1; + /*@i2@*/rare.c_cc[VMIN] = (cc_t)1; (void)tcflush(0, TCIFLUSH); (void)tcsetattr(0, TCSANOW, &rare); } else if (!curses_init()) diff --git a/gpspipe.c b/gpspipe.c index 07051414..8ceea716 100644 --- a/gpspipe.c +++ b/gpspipe.c @@ -23,7 +23,7 @@ * */ -#include /* for time_t */ +#include /* for time_t */ #include "gpsd_config.h" #include @@ -81,8 +81,10 @@ static void open_serial(char *device) /* Clear struct for new port settings. */ /*@i@*/ bzero(&newtio, sizeof(newtio)); +#ifndef S_SPLINT_S /* make it raw */ (void)cfmakeraw(&newtio); +#endif /* S_SPLINT_S */ /* set speed */ /*@i@*/ (void)cfsetospeed(&newtio, BAUDRATE); @@ -339,7 +341,7 @@ int main(int argc, char **argv) struct tm *tmp_now; /*@-type@*//* splint is confused about struct timespec */ - (void)clock_gettime(CLOCK_REALTIME, &now); + /*@i2@*/(void)clock_gettime(CLOCK_REALTIME, &now); tmp_now = localtime((time_t *)&(now.tv_sec)); (void)strftime(tmstr, sizeof(tmstr), format, tmp_now); new_line = 0; diff --git a/gpsutils.c b/gpsutils.c index 52a4b66a..8f51e622 100644 --- a/gpsutils.c +++ b/gpsutils.c @@ -27,6 +27,15 @@ #include #endif +#ifdef S_SPLINT_S +/*@-matchfields@*/ +struct timespec + { + time_t tv_sec; /* Seconds. */ + long tv_nsec; /* Nanoseconds. */ + }; +/*@+matchfields@*/ +#endif /* S_SPLINT_S */ /* * Berkeley implementation of strtod(), inlined to avoid locale problems * with the decimal point and stripped down to an atof()-equivalent. @@ -300,8 +309,8 @@ void gps_merge_fix( /*@ out @*/ struct gps_fix_t *to, timestamp_t timestamp(void) { struct timespec ts; - (void)clock_gettime(CLOCK_REALTIME, &ts); - return (timestamp_t)(ts.tv_sec + ts.tv_nsec * 1e-9); + /*@i2@*/(void)clock_gettime(CLOCK_REALTIME, &ts); + /*@i2@*/return (timestamp_t)(ts.tv_sec + ts.tv_nsec * 1e-9); } time_t mkgmtime(register struct tm * t) @@ -343,7 +352,7 @@ timestamp_t iso8601_to_unix( /*@in@*/ char *isotime) struct tm tm; memset(&tm,0,sizeof(tm)); - dp = strptime(isotime, "%Y-%m-%dT%H:%M:%S", &tm); + /*@i1@*/ dp = strptime(isotime, "%Y-%m-%dT%H:%M:%S", &tm); if (dp != NULL && *dp == '.') usec = strtod(dp, NULL); else @@ -392,7 +401,7 @@ timestamp_t iso8601_to_unix( /*@in@*/ char *isotime) */ (void)snprintf(fractstr, sizeof(fractstr), "%.3f", fractional); /* add fractional part, ignore leading 0; "0.2" -> ".2" */ - (void)snprintf(isotime, len, "%s%sZ",timestr, strchr(fractstr,'.')); + /*@i2@*/(void)snprintf(isotime, len, "%s%sZ",timestr, strchr(fractstr,'.')); return isotime; } /* *INDENT-ON* */ diff --git a/libgps_shm.c b/libgps_shm.c index faa4c548..8eb38041 100644 --- a/libgps_shm.c +++ b/libgps_shm.c @@ -136,7 +136,7 @@ int gps_shm_read(struct gps_data_t *gpsdata) (void)memcpy((void *)gpsdata, (void *)&noclobber, sizeof(struct gps_data_t)); - gpsdata->privdata = private_save; + /*@i1@*/gpsdata->privdata = private_save; PRIVATE(gpsdata)->tick = after; if ((gpsdata->set & REPORT_IS)!=0) { if (gpsdata->fix.mode >= 2) diff --git a/libgpsd_core.c b/libgpsd_core.c index e29fb7d9..33d2a48a 100644 --- a/libgpsd_core.c +++ b/libgpsd_core.c @@ -446,10 +446,10 @@ void gpsd_clear(struct gps_device_t *session) /* set up the context structure for the PPS thread monitor */ memset((void *)&session->pps_thread, 0, sizeof(session->pps_thread)); session->pps_thread.devicefd = session->gpsdata.gps_fd; - session->pps_thread.devicename = session->gpsdata.dev.path; + /*@i2@*/session->pps_thread.devicename = session->gpsdata.dev.path; session->pps_thread.pps_hook = NULL; session->pps_thread.log_hook = ppsthread_log; - session->pps_thread.context = (void *)session; + /*@i4@*/session->pps_thread.context = (void *)session; #endif /* PPS_ENABLE */ session->opentime = time(NULL); @@ -1440,7 +1440,7 @@ gps_mask_t gpsd_poll(struct gps_device_t *session) gps_merge_fix(&session->gpsdata.fix, session->gpsdata.set, &session->newdata); #ifndef NOFLOATS_ENABLE - gpsd_error_model(session, &session->gpsdata.fix, &session->oldfix); + /*@i1@*/gpsd_error_model(session, &session->gpsdata.fix, &session->oldfix); #endif /* NOFLOATS_ENABLE */ /*@+nullderef -nullpass@*/ @@ -1605,7 +1605,7 @@ int gpsd_multipoll(const bool data_ready, /* handle data contained in this packet */ if (device->lexer.type != BAD_PACKET) - handler(device, changed); + /*@i1@*/handler(device, changed); #ifdef __future__ /* diff --git a/serial.c b/serial.c index 1fa78726..282d009c 100644 --- a/serial.c +++ b/serial.c @@ -529,10 +529,8 @@ int gpsd_serial_open(struct gps_device_t *session) #endif if (session->saved_baud != -1) { - /*@i@*/ (void) - cfsetispeed(&session->ttyset, (speed_t) session->saved_baud); - /*@i@*/ (void) - cfsetospeed(&session->ttyset, (speed_t) session->saved_baud); + /*@i@*/(void)cfsetispeed(&session->ttyset, (speed_t)session->saved_baud); + /*@i@*/(void)cfsetospeed(&session->ttyset, (speed_t)session->saved_baud); (void)tcsetattr(session->gpsdata.gps_fd, TCSANOW, &session->ttyset); (void)tcflush(session->gpsdata.gps_fd, TCIOFLUSH); } -- cgit v1.2.1