Clean up most spint errors. All regression tests pass.

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;l2<session->lexer.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 <time.h>                /* for time_t */
+#include <time.h>               /* for time_t */
 #include "gpsd_config.h"
 
 #include <stdio.h>
@@ -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 <QStringList>
 #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);
     }