splint cleanup.

11 files changed, 48 insertions, 26 deletions

diff --git a/bits.c b/bits.c
index bd807348..3468e40f 100644
--- a/bits.c
+++ b/bits.c
@@ -49,7 +49,9 @@ unsigned long long ubits(char buf[], unsigned int start, unsigned int width)
     (void)printf(" = %lld\n", fld);
 #endif /* UDEBUG */
 
+    /*@ -shiftimplementation @*/
     fld &= ~(-1LL << width);
+    /*@ +shiftimplementation @*/
 #ifdef DEBUG
     (void)printf("    after selecting out the bottom %u bits: 0x%llx = %lld\n", 
 		 width, fld, fld);
@@ -71,7 +73,9 @@ signed long long sbits(char buf[], unsigned int start, unsigned int width)
 #ifdef SDEBUG
 	(void)fprintf(stderr, "%llx is signed\n", fld);
 #endif /* SDEBUG */
+	/*@ -shiftimplementation @*/
 	fld |= (-1LL << (width-1));
+	/*@ +shiftimplementation @*/
     }
 #ifdef SDEBUG
     (void)fprintf(stderr, "sbits(%d, %d) returns %lld\n", start, width, (signed long long)fld);
diff --git a/driver_aivdm.c b/driver_aivdm.c
index 4775ff46..a712ce56 100644
--- a/driver_aivdm.c
+++ b/driver_aivdm.c
@@ -35,15 +35,20 @@
  * Parse the data from the device
  */
 
-static void from_sixbit(char *bitvec, int start, int count, char *to)
+static void from_sixbit(char *bitvec, uint start, int count, char *to)
 {
     /*@ +type @*/
+#ifdef S_SPLINT_S
+    /* the real string causes a splint internal error */
+    const char sixchr[] = "abcd";
+#else
     const char sixchr[64] = "@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\\]^- !\"#$%&`()*+,-./0123456789:;<=>?";
+#endif /* S_SPLINT_S */
     int i;
 
     /* six-bit to ASCII */
     for (i = 0; i < count-1; i++)
-	to[i] = sixchr[ubits(bitvec, start + 6*i, 6)];
+	to[i] = sixchr[ubits(bitvec, start + 6*i, 6U)];
     to[count-1] = '\0';
     /* trim spaces on right end */
     for (i = count-2; i >= 0; i--)
@@ -117,12 +122,14 @@ bool aivdm_decode(char *buf, size_t buflen, struct aivdm_context_t *ais_context)
 	if (ch >= 40)
 	    ch -= 8;
 	gpsd_report(LOG_RAW, "%c: %s\n", *cp, sixbits[ch]);
+	/*@ -shiftnegative @*/
 	for (i = 5; i >= 0; i--) {
 	    if ((ch >> i) & 0x01) {
 		ais_context->bits[ais_context->bitlen / 8] |= (1 << (7 - ais_context->bitlen % 8));
 	    }
 	    ais_context->bitlen++;
 	}
+	/*@ +shiftnegative @*/
     }
     /*@ -charint @*/
 
@@ -421,9 +428,10 @@ void  aivdm_dump(struct ais_t *ais, bool scaled, bool labeled, FILE *fp)
     };
 
     if (labeled)
-	(void)fprintf(fp, "type=%d,ri=%d,MMSI=%09d,", ais->id, ais->ri, ais->mmsi);
+	(void)fprintf(fp, "type=%u,ri=%u,MMSI=%09u,", ais->id, ais->ri, ais->mmsi);
     else
-	(void)fprintf(fp, "%d,%d,%09d,", ais->id, ais->ri, ais->mmsi);
+	(void)fprintf(fp, "%u,%u,%09u,", ais->id, ais->ri, ais->mmsi);
+    /*@ -formatconst @*/
     switch (ais->id) {
     case 1:	/* Position Report */
     case 2:
@@ -664,6 +672,7 @@ void  aivdm_dump(struct ais_t *ais, bool scaled, bool labeled, FILE *fp)
 	gpsd_report(LOG_ERROR, "Unparsed AIVDM message type %u.\n",ais->id);
 	break;
     }
+    /*@ +formatconst @*/
 }
 
 #endif /* defined(AIVDM_ENABLE) */
diff --git a/driver_rtcm3.c b/driver_rtcm3.c
index 3a64f216..c30bfb5c 100644
--- a/driver_rtcm3.c
+++ b/driver_rtcm3.c
@@ -121,7 +121,7 @@ void rtcm3_unpack(/*@out@*/struct rtcm3_t *rtcm, char *buf)
 	    rtcm->rtcmtypes.rtcm3_1002.rtk_data[i].L1.ambiguity = (bool)ugrab(8);
 	    rtcm->rtcmtypes.rtcm3_1002.rtk_data[i].L1.CNR = (bool)ugrab(8) * CARRIER_NOISE_RATIO_UNITS;
 	}
-	assert(bitcount == 64 + 74*rtcm->rtcmtypes.rtcm3_1001.header.satcount);
+	assert(bitcount == 64 + 74*rtcm->rtcmtypes.rtcm3_1002.header.satcount);
 	break;
 
     case 1003:	/* GPS Basic RTK, L1 & L2 */
@@ -158,7 +158,7 @@ void rtcm3_unpack(/*@out@*/struct rtcm3_t *rtcm, char *buf)
 		rtcm->rtcmtypes.rtcm3_1003.rtk_data[i].L2.rangediff  = temp * PSEUDORANGE_DIFF_RESOLUTION;
 	    rtcm->rtcmtypes.rtcm3_1003.rtk_data[i].L2.locktime = (unsigned char)sgrab(7);
 	}
-	assert(bitcount == 64 + 101*rtcm->rtcmtypes.rtcm3_1001.header.satcount);
+	assert(bitcount == 64 + 101*rtcm->rtcmtypes.rtcm3_1003.header.satcount);
 	break;
 
     case 1004:	/* GPS Extended RTK, L1 & L2 */
@@ -199,7 +199,7 @@ void rtcm3_unpack(/*@out@*/struct rtcm3_t *rtcm, char *buf)
 	    rtcm->rtcmtypes.rtcm3_1004.rtk_data[i].L2.ambiguity = (bool)ugrab(8);
 	    rtcm->rtcmtypes.rtcm3_1004.rtk_data[i].L2.CNR = (bool)ugrab(8) * CARRIER_NOISE_RATIO_UNITS;
 	}
-	assert(bitcount == 64 + 125*rtcm->rtcmtypes.rtcm3_1001.header.satcount);
+	assert(bitcount == 64 + 125*rtcm->rtcmtypes.rtcm3_1004.header.satcount);
 	break;
 
     case 1005:	/* Stationary Antenna Reference Point, No Height Information */
@@ -316,7 +316,7 @@ void rtcm3_unpack(/*@out@*/struct rtcm3_t *rtcm, char *buf)
 	    rtcm->rtcmtypes.rtcm3_1010.rtk_data[i].L1.ambiguity = (bool)ugrab(7);
 	    rtcm->rtcmtypes.rtcm3_1010.rtk_data[i].L1.CNR = (bool)ugrab(8) * CARRIER_NOISE_RATIO_UNITS;
 	}
-	assert(bitcount == 61 + 79*rtcm->rtcmtypes.rtcm3_1009.header.satcount);
+	assert(bitcount == 61 + 79*rtcm->rtcmtypes.rtcm3_1010.header.satcount);
 	break;
 
     case 1011:	/* GLONASS Basic RTK, L1 & L2 */
@@ -359,7 +359,7 @@ void rtcm3_unpack(/*@out@*/struct rtcm3_t *rtcm, char *buf)
 	    rtcm->rtcmtypes.rtcm3_1011.rtk_data[i].L2.ambiguity = (bool)ugrab(7);
 	    rtcm->rtcmtypes.rtcm3_1011.rtk_data[i].L2.CNR = (bool)ugrab(8) * CARRIER_NOISE_RATIO_UNITS;
 	}
-	assert(bitcount == 61 + 107*rtcm->rtcmtypes.rtcm3_1009.header.satcount);
+	assert(bitcount == 61 + 107*rtcm->rtcmtypes.rtcm3_1011.header.satcount);
 	break;
 
     case 1012:	/* GLONASS Extended RTK, L1 & L2 */
@@ -397,7 +397,7 @@ void rtcm3_unpack(/*@out@*/struct rtcm3_t *rtcm, char *buf)
 		rtcm->rtcmtypes.rtcm3_1012.rtk_data[i].L2.rangediff  = temp * PSEUDORANGE_DIFF_RESOLUTION;
 	    rtcm->rtcmtypes.rtcm3_1012.rtk_data[i].L2.locktime = (unsigned char)sgrab(7);
 	}
-	assert(bitcount == 61 + 130*rtcm->rtcmtypes.rtcm3_1009.header.satcount);
+	assert(bitcount == 61 + 130*rtcm->rtcmtypes.rtcm3_1012.header.satcount);
 	break;
 
     case 1013:	/* System Parameters */
@@ -725,10 +725,10 @@ void rtcm3_dump(struct rtcm3_t *rtcm, FILE *fp)
 
 	case 1014:
 	    (void)fprintf(fp,
-			  "    netid=%u subnetid=%d statcount=%d master=%d aux=%d lat=%f, lon=%f, alt=%f\n",
+			  "    netid=%u subnetid=%u statcount=%u master=%u aux=%u lat=%f, lon=%f, alt=%f\n",
 			  rtcm->rtcmtypes.rtcm3_1014.network_id,
 			  rtcm->rtcmtypes.rtcm3_1014.subnetwork_id,
-			  (int)rtcm->rtcmtypes.rtcm3_1014.stationcount,
+			  (uint)rtcm->rtcmtypes.rtcm3_1014.stationcount,
 			  rtcm->rtcmtypes.rtcm3_1014.master_id,
 			  rtcm->rtcmtypes.rtcm3_1014.aux_id,
 			  rtcm->rtcmtypes.rtcm3_1014.d_lat,
diff --git a/drivers.c b/drivers.c
index 18204cc2..5d608c2f 100644
--- a/drivers.c
+++ b/drivers.c
@@ -48,7 +48,7 @@ gps_mask_t nmea_parse_input(struct gps_device_t *session)
 	    if (session->packet.type == (*dp)->packet_type) {
 		gpsd_report(LOG_WARN, "%s packet seen when NMEA expected.\n",
 			    (*dp)->type_name);
-		gpsd_switch_driver(session, (*dp)->type_name);
+		(void)gpsd_switch_driver(session, (*dp)->type_name);
 		return (*dp)->parse_packet(session);
 	    }
 	}
@@ -1065,7 +1065,7 @@ gps_mask_t aivdm_parse(struct gps_device_t *session)
 	 * widen it when ready for production.
 	 */
 	(void)snprintf(session->gpsdata.tag, sizeof(session->gpsdata.tag),
-		       "AIS%d", session->driver.aivdm.decoded.mmsi);
+		       "AIS%u", session->driver.aivdm.decoded.mmsi);
 
 	/* FIXME: actual driver code goes here if we're going to report fixes from these */
     }
diff --git a/gpsd.c b/gpsd.c
index fbd56e40..546a478e 100644
--- a/gpsd.c
+++ b/gpsd.c
@@ -1322,19 +1322,20 @@ static void handle_control(int sfd, char *buf)
 	    }
 	}
     } else if (buf[0] == '&') {
-	ssize_t len;
 	p = snarfline(buf+1, &stash);
 	eq = strchr(stash, '=');
 	if (eq == NULL) {
 	    gpsd_report(LOG_WARN,"<= control(%d): ill-formed command \n", sfd);
 	    ignore_return(write(sfd, "ERROR\n", 6));
 	} else {
+	    size_t len;
+	    int st;
 	    *eq++ = '\0';
 	    len = strlen(eq)+5;
 	    if ((chp = find_device(stash)) != NULL) {
 		/* NOTE: this destroys the original buffer contents */
-		len = (ssize_t)gpsd_hexpack(eq, eq, len);
-		if (len < 0)
+		st = gpsd_hexpack(eq, eq, len);
+		if (st < 0)
 		    gpsd_report(LOG_INF,"<= control(%d): invalid hex string (error %zd)\n", sfd, len);
 		else
 		{
diff --git a/gpsd.h-tail b/gpsd.h-tail
index 88cb7eec..4cf6788f 100644
--- a/gpsd.h-tail
+++ b/gpsd.h-tail
@@ -214,7 +214,7 @@ struct gps_type_t {
 				     speed_t speed, char parity, int stopbits);
     /*@null@*/void (*mode_switcher)(struct gps_device_t *session, int mode);
     /*@null@*/bool (*rate_switcher)(struct gps_device_t *session, double rate);
-    int min_cycle;
+    double min_cycle;
     /*@null@*/void (*revert)(struct gps_device_t *session);
 #endif /* ALLOW_RECONFIGURE */
     /*@null@*/void (*wrapup)(struct gps_device_t *session);
@@ -421,7 +421,7 @@ extern void gpsd_interpret_subframe(struct gps_device_t *, unsigned int[]);
 extern int gpsd_hexdump_level;
 extern /*@ observer @*/ char *gpsd_hexdump(/*@null@*/const void *, size_t);
 extern /*@ observer @*/ char *gpsd_hexdump_wrapper(/*@null@*/const void *, size_t, int);
-extern int gpsd_hexpack(char *, char *, size_t);
+extern int gpsd_hexpack(/*@in@*/char *, /*@out@*/char *, size_t);
 extern int hex2bin(char *);
 extern ssize_t hex_escapes(/*@out@*/char *cooked, const char *raw);
 extern void ntpd_link_activate(struct gps_device_t *session);
diff --git a/gpsdecode.c b/gpsdecode.c
index 2c46f2c5..4b35c743 100644
--- a/gpsdecode.c
+++ b/gpsdecode.c
@@ -66,8 +66,10 @@ static void decode(FILE *fpin, FILE *fpout)
 	    rtcm3_dump(&rtcm3, stdout);
 	}
 	else if (lexer.type == AIVDM_PACKET) {
+	    /*@ -uniondef */
 	    if (aivdm_decode((char *)lexer.outbuffer, lexer.outbuflen, &aivdm))
 		aivdm_dump(&aivdm.decoded, scaled, labeled, stdout);
+	    /*@ +uniondef */
 	}
     }
 }
diff --git a/gpsmon.c b/gpsmon.c
index 73d87935..55fb1d4c 100644
--- a/gpsmon.c
+++ b/gpsmon.c
@@ -846,22 +846,26 @@ int main (int argc, char **argv)
 		if (active == NULL)
 		    monitor_complain("No device defined yet");
 		else {
-		    len = gpsd_hexpack(arg, (char*)buf, strlen(arg));
-		    if (len < 0)
-			monitor_complain("Invalid hex string (error %d)", len);
+		    /*@ -compdef @*/
+		    int st = gpsd_hexpack(arg, (char*)buf, strlen(arg));
+		    if (st < 0)
+			monitor_complain("Invalid hex string (error %d)", st);
 		    else if ((*active)->driver->control_send == NULL)
 			monitor_complain("Device type has no control-send method.");
-		    else if (!monitor_control_send(buf, (size_t)len))
+		    else if (!monitor_control_send(buf, (size_t)st))
 			monitor_complain("Control send failed.");
 		}
+		    /*@ +compdef @*/
 		break;
 
 	    case 'X':				/* send raw packet */
+		/*@ -compdef @*/
 		len = (ssize_t)gpsd_hexpack(arg, (char*)buf, strlen(arg));
 		if (len < 0)
 		    monitor_complain("Invalid hex string (error %d)", len);
 		else if (!monitor_raw_send(buf, (size_t)len))
 		    monitor_complain("Raw send failed.");
+		/*@ +compdef @*/
 		break;
 #endif /* ALLOW_CONTROLSEND */
 
diff --git a/hex.c b/hex.c
index f09f6159..5addeaeb 100644
--- a/hex.c
+++ b/hex.c
@@ -56,6 +56,7 @@ int gpsd_hexpack(char *src, char *dst, size_t len){
 /* hex2bin source string to destination - destination can be same as source */ 
     int i, k, l;
 
+    /*@ -mustdefine @*/
     l = (int)(strlen(src) / 2);
     if ((l < 1) || ((size_t)l > len))
 	return -2;
@@ -67,6 +68,7 @@ int gpsd_hexpack(char *src, char *dst, size_t len){
 	else
 	    return -1;
     return l;
+    /*@ +mustdefine @*/
 }
 
 /*@ +charint -shiftimplementation @*/
diff --git a/libgps.c b/libgps.c
index 2cf860e5..a8fc928a 100644
--- a/libgps.c
+++ b/libgps.c
@@ -72,7 +72,7 @@ void gps_set_raw_hook(struct gps_data_t *gpsdata,
     gpsdata->raw_hook = hook;
 }
 
-/*@ -branchstate -usereleased @*/
+/*@ -branchstate -usereleased -mustfreefresh @*/
 static void gps_unpack(char *buf, struct gps_data_t *gpsdata)
 /* unpack a gpsd response into a status structure, buf must be writeable */
 {
@@ -441,7 +441,7 @@ static void gps_unpack(char *buf, struct gps_data_t *gpsdata)
 	gpsdata->thread_hook(gpsdata, buf, strlen(buf), 1);
 }
 /*@ +nullstate +compdef @*/
-/*@ -branchstate +usereleased @*/
+/*@ -branchstate +usereleased +mustfreefresh @*/
 
 /*
  * return: 0, success
diff --git a/libgpsd_core.c b/libgpsd_core.c
index 72b004d7..4a067b6d 100644
--- a/libgpsd_core.c
+++ b/libgpsd_core.c
@@ -705,7 +705,7 @@ gps_mask_t gpsd_poll(struct gps_device_t *session)
 	if (session->packet.type >= COMMENT_PACKET) {
 	    for (dp = gpsd_drivers; *dp; dp++)
 		if (session->packet.type == (*dp)->packet_type) {
-		    gpsd_switch_driver(session, (*dp)->type_name);
+		    (void)gpsd_switch_driver(session, (*dp)->type_name);
 		    break;
 		}
 	} else if (!gpsd_next_hunt_setting(session))