splint cleanup. All regressiion tests pass.

13 files changed, 32 insertions, 29 deletions

diff --git a/driver_nmea2000.c b/driver_nmea2000.c
index cab2ec4f..628abd7d 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);
 }
diff --git a/gps.h b/gps.h
index a81f7f3f..b6ee0f63 100644
--- a/gps.h
+++ b/gps.h
@@ -2065,7 +2065,7 @@ extern double earth_distance_and_bearings(double, double, double, double,
 					  /*@null@*//*@out@*/double *,
 					  /*@null@*//*@out@*/double *);
 extern double wgs84_separation(double, double);
-extern int timespec_str( struct timespec *, char *, int );
+extern int timespec_str(struct timespec *, /*@out@*/char *, int);
 
 /* some multipliers for interpreting GPS output */
 #define METERS_TO_FEET	3.2808399	/* Meters to U.S./British feet */
diff --git a/gpsctl.c b/gpsctl.c
index 4ff29caa..434be095 100644
--- a/gpsctl.c
+++ b/gpsctl.c
@@ -295,6 +295,7 @@ int main(int argc, char **argv)
 	    break;
 	case 'R':		/* remove the SHM export segment */
 #ifdef SHM_EXPORT_ENABLE
+	    /*@-nullpass@*/
 	    status = shmget(GPSD_KEY, 0, 0);
 	    if (status == -1) {
 		gpsd_report(&context.errout, LOG_WARN,
@@ -309,9 +310,9 @@ int main(int argc, char **argv)
 		    exit(1);
 		}
 	    }
+	    /*@+nullpass@*/
 	    exit(0);
 #endif /* SHM_EXPORT_ENABLE */
-	    break;
 	case 'T':		/* set the timeout on packet recognition */
 	    timeout = (unsigned)atoi(optarg);
 	    explicit_timeout = true;
diff --git a/gpsdecode.c b/gpsdecode.c
index f31a59f6..ece81d57 100644
--- a/gpsdecode.c
+++ b/gpsdecode.c
@@ -621,7 +621,7 @@ static void decode(FILE *fpin, FILE*fpout)
 			break;
 		    }
 		}
-		printf("%s (%d): %d\n", np, i-1, (unsigned int)minima[i]);
+		printf("%s (%d): %u\n", np, i-1, (unsigned int)minima[i]);
 	    }
 	}
     }
diff --git a/gpsmon.c b/gpsmon.c
index a5c88c34..f01d16f6 100644
--- a/gpsmon.c
+++ b/gpsmon.c
@@ -673,7 +673,7 @@ static void gpsmon_hook(struct gps_device_t *device, gps_mask_t changed UNUSED)
 	    complain("Ill-formed PPS packet: %d", status);
 	    buf[0] = '\0';
 	} else {
-	    /*@-type@*/ /* splint is confused about struct timespec */
+	    /*@-type -noeffect@*/ /* splint is confused about struct timespec */
 	    struct timespec timedelta;
 	    TS_SUB( &timedelta, &noclobber.timedrift.real, 
 		&noclobber.timedrift.clock);
@@ -687,7 +687,7 @@ static void gpsmon_hook(struct gps_device_t *device, gps_mask_t changed UNUSED)
 			      (long)noclobber.timedrift.real.tv_nsec,
 			      (long)timedelta.tv_sec,
                               (long)timedelta.tv_nsec);
-	    /*@+type@*/
+	    /*@+type +noeffect@*/
 
 	    (void)strlcpy(buf, PPSBAR, sizeof(buf));
 	    /* coverity[missing_lock] */
diff --git a/gpsutils.c b/gpsutils.c
index 388a7bae..8c9525ff 100644
--- a/gpsutils.c
+++ b/gpsutils.c
@@ -490,11 +490,12 @@ double earth_distance(double lat1, double lon1, double lat2, double lon2)
  * return negative for error
  * otherwise the number of chars in buf, excluding trailing \0
 */
-int timespec_str( struct timespec *ts, char *buf, int buf_size )
+int timespec_str(struct timespec *ts, /*@out@*/char *buf, int buf_size)
 {
     int ret;
     char sign = ' ';
 
+    /*@-type@*//* splint is confused about timespec*/
     if ( (0 > ts->tv_nsec ) || ( 0 > ts->tv_sec ) ) {
 	sign = '-';
     }
@@ -502,5 +503,6 @@ int timespec_str( struct timespec *ts, char *buf, int buf_size )
 			  sign,
 			  (long)labs(ts->tv_sec),
 			  (long)labs(ts->tv_nsec));
+    /*@+type@*/
     return ret;
 }
diff --git a/libgpsd_core.c b/libgpsd_core.c
index 7d8d16fe..e0d605a0 100644
--- a/libgpsd_core.c
+++ b/libgpsd_core.c
@@ -322,8 +322,8 @@ void gpsd_init(struct gps_device_t *session, struct gps_context_t *context,
 {
     /* clear some times */
     session->last_fixtime.real = 0.0;
-    session->last_fixtime.clock.tv_sec = 0;
-    session->last_fixtime.clock.tv_nsec = 0;
+    /*@i2@*/session->last_fixtime.clock.tv_sec = 0;
+    /*@i2@*/session->last_fixtime.clock.tv_nsec = 0;
 #ifdef PPS_ENABLE
     memset( (void *)&session->ppslast, 0, sizeof(session->ppslast));
     session->ppscount = 0;
@@ -424,8 +424,8 @@ void gpsd_clear(struct gps_device_t *session)
     memset( (void *)&session->driver, '\0', sizeof(session->driver));
     /* clear some times */
     session->last_fixtime.real = 0.0;
-    session->last_fixtime.clock.tv_sec = 0;
-    session->last_fixtime.clock.tv_nsec = 0;
+    /*@i2@*/session->last_fixtime.clock.tv_sec = 0;
+    /*@i2@*/session->last_fixtime.clock.tv_nsec = 0;
 #ifdef PPS_ENABLE
     memset( (void *)&session->ppslast, 0, sizeof(session->ppslast));
     session->ppscount = 0;
@@ -1110,7 +1110,6 @@ gps_mask_t gpsd_poll(struct gps_device_t *session)
 {
     ssize_t newlen;
     bool driver_change = false;
-    float alpha;
 
     gps_clear_fix(&session->newdata);
 
diff --git a/monitor_nmea.c b/monitor_nmea.c
index b8461ed7..6a632006 100644
--- a/monitor_nmea.c
+++ b/monitor_nmea.c
@@ -325,7 +325,7 @@ static void nmea_update(void)
 
 #ifdef PPS_ENABLE
     /*@-compdef@*/
-    /*@-type@*/ /* splint is confused about struct timespec */
+    /*@-type -noeffect@*/ /* splint is confused about struct timespec */
     if (pps_thread_lastpps(&session, &drift) > 0) {
 	/* NOTE: can not use double here due to precision requirements */
 	struct timespec timedelta;
@@ -341,7 +341,7 @@ static void nmea_update(void)
         }
 	(void)wnoutrefresh(gpgsawin);
     }
-    /*@+type@*/
+    /*@+type +noeffect@*/
     /*@+compdef@*/
 #endif /* PPS_ENABLE */
 }
diff --git a/monitor_sirf.c b/monitor_sirf.c
index 16371d50..f99a85ac 100644
--- a/monitor_sirf.c
+++ b/monitor_sirf.c
@@ -589,23 +589,23 @@ static void sirf_update(void)
 
 #ifdef PPS_ENABLE
     /*@-compdef@*/
-    /*@-type@*/ /* splint is confused about struct timespec */
+    /*@-type -noeffect@*/ /* splint is confused about struct timespec */
     if (pps_thread_lastpps(&session, &drift) > 0) {
 	/* NOTE: can not use double here due to precision requirements */
 	struct timespec timedelta;
-        char buf[22];
+        char buf2[22];
 	TS_SUB( &timedelta, &drift.clock, &drift.real);
         if ( 86400 < (long)labs(timedelta.tv_sec) ) {
 	    /* more than one day off, overflow */
             /* need a bigger field to show it */
 	    (void)mvwprintw(mid7win, 2, 39, "> 1 day");
         } else {
-	    (void)timespec_str( &timedelta, buf, sizeof(buf) );
-	    (void)mvwprintw(mid7win, 4, 39, "%s", buf);
+	    (void)timespec_str( &timedelta, buf2, sizeof(buf2) );
+	    (void)mvwprintw(mid7win, 4, 39, "%s", buf2);
         }
 	(void)wnoutrefresh(mid7win);
     }
-    /*@+type@*/
+    /*@+type +noeffect@*/
     /*@+compdef@*/
 #endif /* PPS_ENABLE */
 }
diff --git a/monitor_ubx.c b/monitor_ubx.c
index 4fdfb58a..8b4101e2 100644
--- a/monitor_ubx.c
+++ b/monitor_ubx.c
@@ -256,23 +256,23 @@ static void ubx_update(void)
 
 #ifdef PPS_ENABLE
     /*@-compdef@*/
-    /*@-type@*/ /* splint is confused about struct timespec */
+    /*@-type -noeffect@*/ /* splint is confused about struct timespec */
     if (pps_thread_lastpps(&session, &drift) > 0) {
 	/* NOTE: can not use double here due to precision requirements */
 	struct timespec timedelta;
-        char buf[22];
+        char buf2[22];
 	TS_SUB( &timedelta, &drift.clock, &drift.real);
         if ( 86400 < (long)labs(timedelta.tv_sec) ) {
 	    /* more than one day off, overflow */
             /* need a bigger field to show it */
 	    (void)mvwprintw(ppswin, 1, 13, "> 1 day");
         } else {
-	    (void)timespec_str( &timedelta, buf, sizeof(buf) );
-	    (void)mvwprintw(ppswin, 1, 13, "%s", buf);
+	    (void)timespec_str( &timedelta, buf2, sizeof(buf2) );
+	    (void)mvwprintw(ppswin, 1, 13, "%s", buf2);
         }
 	(void)wnoutrefresh(ppswin);
     }
-    /*@+type@*/
+    /*@+type +noeffect@*/
     /*@+compdef@*/
 #endif /* PPS_ENABLE */
 }
diff --git a/packet.c b/packet.c
index be55cedd..82bd2343 100644
--- a/packet.c
+++ b/packet.c
@@ -198,11 +198,11 @@ static bool character_pushback(struct gps_lexer_t *lexer, unsigned int newstate)
     lexer->state = newstate;
     if (lexer->errout.debug >= LOG_RAW + 2)
     {
-	unsigned int c = *lexer->inbufptr;
+	unsigned char c = *lexer->inbufptr;
 	gpsd_report(&lexer->errout, LOG_RAW + 2,
 		"%08ld: character '%c' [%02x]  pushed back, state set to %s\n",
 		lexer->char_counter,
-		(isprint(c) ? c : '.'), c,
+		(isprint((int)c) ? c : '.'), c,
 		state_table[lexer->state]);
     }
 
@@ -979,7 +979,6 @@ static bool nextstate(struct gps_lexer_t *lexer, unsigned char c)
 	if ((c & 0xFC) == 0) {
 	    lexer->length = (size_t) (c << 8);
 	    lexer->state = RTCM3_LEADER_2;
-	    break;
 	} else
 	    return character_pushback(lexer, GROUND_STATE);
 	break;
diff --git a/ppsthread.c b/ppsthread.c
index d0cf9ab6..be5c92e4 100644
--- a/ppsthread.c
+++ b/ppsthread.c
@@ -89,7 +89,9 @@ void pps_early_init( struct gps_context_t * context ) {
     int err;
 
     /*@ -unrecog  (splint has no pthread declarations as yet) @*/
+    /*@ -nullpass @*/
     err = pthread_mutex_init(&ppslast_mutex, NULL);
+    /*@ +nullpass@ */
     /*@ +unrecog @*/
     if ( 0 != err ) {
 	gpsd_report(&context->errout, LOG_ERROR,
@@ -680,7 +682,6 @@ static /*@null@*/ void *gpsd_ppsmonitor(void *arg)
 			    strerror(errno));
 		}
 		/*@ +unrecog @*/
-		/*@+compdef@*/
 		/*@-type@*/ /* splint is confused about struct timespec */
 		(void)timespec_str( &drift.clock, ts_str1, sizeof(ts_str1) );
 		(void)timespec_str( &drift.real, ts_str2, sizeof(ts_str2) );
@@ -688,6 +689,7 @@ static /*@null@*/ void *gpsd_ppsmonitor(void *arg)
 			    "PPS hooks called with %.20s clock: %s real: %s\n",
 			    log1, ts_str1, ts_str2);
 		/*@+type@*/
+		/*@+compdef@*/
             }
 	    /*@-type@*/ /* splint is confused about struct timespec */
 	    (void)timespec_str( &clock_ts, ts_str1, sizeof(ts_str1) );
diff --git a/serial.c b/serial.c
index df8ab303..83cea6df 100644
--- a/serial.c
+++ b/serial.c
@@ -578,7 +578,7 @@ int gpsd_serial_open(struct gps_device_t *session)
     {
 	int oldfl = fcntl(session->gpsdata.gps_fd, F_GETFL);
 	if (oldfl != -1)
-	    fcntl(session->gpsdata.gps_fd, F_SETFL, oldfl & ~O_NONBLOCK);
+	    (void)fcntl(session->gpsdata.gps_fd, F_SETFL, oldfl & ~O_NONBLOCK);
     }