This diff goes most of the way to getting us splint-clean again.

27 files changed, 127 insertions, 86 deletions

diff --git a/.splintrc b/.splintrc
index 71321211..f3af2260 100644
--- a/.splintrc
+++ b/.splintrc
@@ -26,3 +26,4 @@
 -DB115200=0010011
 -DCRTSCTS=0x00020000
 -DONLCR=0x00000002
+-D__gnuc_va_list=va_list
diff --git a/Makefile.am b/Makefile.am
index 448896a1..ea83b172 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -340,7 +340,7 @@ libgps: libgps.c .libs/libgps.a
 
 # Report splint warnings
 SPLINTOPTS = -I/usr/include/dbus-1.0/
-splint:
+splint: gpsd.h packet_names.h
 	@echo "Running splint on daemon and libraries..."
 	-splint $(SPLINTOPTS) -exportlocal -redef $(gpsd_c_sources) $(libgpsd_c_sources)
 	@echo "Running splint on xgps..."
diff --git a/bits.c b/bits.c
index e12891a2..dc508b88 100644
--- a/bits.c
+++ b/bits.c
@@ -25,7 +25,7 @@ unsigned long long ubits(char buf[], unsigned int start, unsigned int width)
     unsigned int i;
     unsigned end;
 
-    assert(width <= sizeof(long long) * BITS_PER_BYTE);
+    /*@i1@*/assert(width <= sizeof(long long) * BITS_PER_BYTE);
     for (i = start / BITS_PER_BYTE; i < (start + width + BITS_PER_BYTE - 1) / BITS_PER_BYTE; i++) {
 	fld <<= BITS_PER_BYTE;
 	fld |= (unsigned char)buf[i];
@@ -59,11 +59,13 @@ signed long long sbits(char buf[], unsigned int start, unsigned int width)
     unsigned long long un = ubits(buf, start, width);
     signed long long fld;
 
+    /*@ +relaxtypes */
     if (un & (1 << width))
 	fld = -(un & ~(1 << width));
     else
 	fld = (signed long long)un;
     
     return fld;
+    /*@ -relaxtypes */
 }
 
diff --git a/bits_test.c b/bits_test.c
index 25f35f3a..4d2089ff 100644
--- a/bits_test.c
+++ b/bits_test.c
@@ -109,8 +109,8 @@ int main(void)
 
     (void)fputs("Test data:", stdout);
     for (sp = buf; sp < buf + 28; sp++)
-	printf(" %02x", *sp);
-    putc('\n', stdout);
+	(void)printf(" %02x", *sp);
+    (void)putc('\n', stdout);
 
     /* big-endian test */
     printf("Big-endian:\n");
diff --git a/cgps.c b/cgps.c
index b1b714b3..0cf161dd 100644
--- a/cgps.c
+++ b/cgps.c
@@ -142,8 +142,10 @@ static int display_sats;
    desirable (in case the don't notice the subtle change from "(mag)"
    to "(true)" on their display).
  */
-static float true2magnetic(double lat, double lon, double heading) {
+static float true2magnetic(double lat, double lon, double heading)
+{
   /* Western Europe */
+  /*@ -evalorder +relaxtypes @*/
   if((lat > 36.0) && (lat < 68.0) &&
      (lon > -10.0) && (lon < 28.0)) {
     return( 10.4768771667158 - (0.507385322418858 * lon) + (0.00753170031703826 * pow(lon, 2))
@@ -169,6 +171,7 @@ static float true2magnetic(double lat, double lon, double heading) {
   }
   magnetic_flag=0;
   return(heading);
+  /*@ +evalorder -relaxtypes @*/
 }
 
 /* Function to call when we're all done.  Does a bit of clean-up. */
diff --git a/dgpsip.c b/dgpsip.c
index 2da757eb..27abb9b5 100644
--- a/dgpsip.c
+++ b/dgpsip.c
@@ -35,7 +35,7 @@ int dgpsip_open(struct gps_context_t *context, const char *dgpsserver)
 	(void)gethostname(hn, sizeof(hn));
 	/* greeting required by some RTCM104 servers; others will ignore it */
 	(void)snprintf(buf,sizeof(buf), "HELO %s gpsd %s\r\nR\r\n",hn,VERSION);
-	if (write(context->dsock, buf, strlen(buf)) == strlen(buf))
+	if (write(context->dsock, buf, strlen(buf)) == (ssize_t)strlen(buf))
 	    context->dgnss_service = dgnss_dgpsip;
 	else
 	    gpsd_report(LOG_ERROR, "hello to DGPS server %s failed\n", dgpsserver);
@@ -64,7 +64,7 @@ void dgpsip_report(struct gps_device_t *session)
 			   session->gpsdata.fix.latitude, 
 			   session->gpsdata.fix.longitude, 
 			   session->gpsdata.fix.altitude);
-	    if (write(session->context->dsock, buf, strlen(buf)) == strlen(buf))
+	    if (write(session->context->dsock, buf, strlen(buf)) == (ssize_t)strlen(buf))
 		gpsd_report(LOG_IO, "=> dgps %s", buf);
 	    else
 		gpsd_report(LOG_IO, "write to dgps FAILED");
diff --git a/display.c b/display.c
index 9d167b6a..2122acd0 100644
--- a/display.c
+++ b/display.c
@@ -38,8 +38,7 @@
 
 static Widget draww, appshell;
 static GC drawGC;
-static Dimension width, height;
-static int diameter;
+static Dimension width, height, diameter;
 static Pixmap pixmap;
 
 /*@ -usedef -compdef -mustfreefresh @*/
@@ -139,7 +138,7 @@ draw_graphics(struct gps_data_t *gpsdata)
 
 		/* draw something in the center */
 		set_color("Grey");
-		draw_arc(width / 2, height / 2, 6);
+		draw_arc((int)(width / 2), (int)(height / 2), 6);
 
 		/* draw the 45 degree circle */
 #ifdef PCORRECT
@@ -147,11 +146,11 @@ draw_graphics(struct gps_data_t *gpsdata)
 #else
 #define FF	0.5
 #endif
-		draw_arc(width / 2, height / 2, (unsigned)((i - RM) * FF));
+		draw_arc((int)(width / 2), (int)(height / 2), (unsigned)((i - RM) * FF));
 #undef FF
 
 		set_color("Black");
-		draw_arc(width / 2, height / 2, (unsigned)(i - RM));
+		draw_arc((int)(width / 2), (int)(height / 2), (unsigned)(i - RM));
 
 		pol2cart(0, 0, &x, &y);
 		set_color("Black");
diff --git a/drivers.c b/drivers.c
index 8afbd9ae..e007fd0c 100644
--- a/drivers.c
+++ b/drivers.c
@@ -32,7 +32,7 @@ ssize_t pass_rtcm(struct gps_device_t *session, char *buf, size_t rtcmbytes)
 
 #ifdef UBX_ENABLE
     extern gps_mask_t ubx_parse(struct gps_device_t *session, unsigned char *buf, size_t len);
-    extern bool ubx_write(int fd, unsigned char msg_class, unsigned char msg_id, unsigned char *msg, unsigned short data_len);
+    extern bool ubx_write(int fd, unsigned int msg_class, unsigned int msg_id, unsigned char *msg, unsigned short data_len);
     extern void ubx_catch_model(struct gps_device_t *session, unsigned char *buf, size_t len);
 #endif /* UBX_ENABLE */
 
@@ -228,7 +228,7 @@ static void nmea_probe_subtype(struct gps_device_t *session, unsigned int seq)
 #ifdef UBX_ENABLE
     case 7:
 	/* probe for UBX -- query software version */
-	ubx_write(session->gpsdata.gps_fd, 0x0a, 0x04, NULL, 0);
+	(void)ubx_write(session->gpsdata.gps_fd, 0x0au, 0x04, NULL, 0);
 	break;
 #endif /* UBX_ENABLE */
 #ifdef MKT3301_ENABLE
diff --git a/gps.h b/gps.h
index c0b29e2f..79cfab85 100644
--- a/gps.h
+++ b/gps.h
@@ -587,7 +587,7 @@ struct gps_data_t {
     void (*thread_hook)(struct gps_data_t *, char *, size_t len, int level);/* Thread-callback hook for GPS data. */
 };
 
-extern struct gps_data_t *gps_open(const char *host, const char *port);
+extern /*@null@*/ struct gps_data_t *gps_open(const char *host, const char *port);
 int gps_close(struct gps_data_t *);
 int gps_query(struct gps_data_t *gpsdata, const char *fmt, ... );
 int gps_poll(struct gps_data_t *gpsdata);
diff --git a/gpsd.c b/gpsd.c
index 0c5de188..96c1307d 100644
--- a/gpsd.c
+++ b/gpsd.c
@@ -135,6 +135,7 @@ static int daemonize(void)
     int fd;
     pid_t pid;
 
+    /*@ -type @*/	/* weirdly, splint 3.1.2 is confused by fork() */
     switch (pid = fork()) {
     case -1:
 	return -1;
@@ -143,6 +144,7 @@ static int daemonize(void)
     default:	/* parent side */
 	exit(0);
     }
+    /*@ +type @*/
 
     if (setsid() == -1)
 	return -1;
@@ -236,7 +238,7 @@ static int passivesock(char *service, char *protocol, int qlen)
     struct sockaddr_in sin;
     int s, type, proto, one = 1;
 
-    /*@ -mustfreefresh @*/
+    /*@ -mustfreefresh +matchanyintegral @*/
     memset((char *) &sin, 0, sizeof(sin));
     sin.sin_family = (sa_family_t)AF_INET;
     if (listen_global)
@@ -278,7 +280,7 @@ static int passivesock(char *service, char *protocol, int qlen)
 	return -1;
     }
     return s;
-    /*@ +mustfreefresh @*/
+    /*@ +mustfreefresh -matchanyintegral @*/
 }
 
 static int filesock(char *filename)
@@ -293,7 +295,7 @@ static int filesock(char *filename)
     }
     (void)strlcpy(addr.sun_path, filename, 104); /* from sys/un.h */
     /*@i1@*/addr.sun_family = AF_UNIX;
-    (void)bind(sock, (struct sockaddr *) &addr,  (int)sizeof(addr));
+    (void)bind(sock, (struct sockaddr *) &addr,  (socklen_t)sizeof(addr));
     if (listen(sock, QLEN) < 0) {
 	gpsd_report(LOG_ERROR, "can't listen on local socket %s\n", filename);
 	return -1;
@@ -620,11 +622,13 @@ static bool assign_channel(struct subscriber_t *user)
 	    FD_SET(user->device->gpsdata.gps_fd, &all_fds);
 	    adjust_max_fd(user->device->gpsdata.gps_fd, true);
 	    if (user->watcher && !user->tied) {
+		/*@ -sefparams @*/
 		assert(write(user->fd, "GPSD,F=", 7) != -1);
 		assert(write(user->fd,
 			     user->device->gpsdata.gps_device,
 			     strlen(user->device->gpsdata.gps_device)) != -1);
 		assert(write(user->fd, "\r\n", 2) != -1);
+		/*@ +sefparams @*/
 	    }
 	}
     }
@@ -633,7 +637,10 @@ static bool assign_channel(struct subscriber_t *user)
 	char buf[NMEA_MAX];
 	(void)snprintf(buf, sizeof(buf), "GPSD,X=%f,I=%s\r\n",
 		       timestamp(), gpsd_id(user->device));
+	/*@ -sefparams +matchanyintegral @*/
 	assert(write(user->fd, buf, strlen(buf)) == strlen(buf));
+	/*@ +sefparams -matchanyintegral @*/
+
     }
     return true;
 }
@@ -732,7 +739,7 @@ static int handle_gpsd_request(struct subscriber_t* sub, char *buf, int buflen)
 			/* zero parity breaks the next snprintf */
 			sub->device->gpsdata.parity = (unsigned)'N';
 		}
-		(void)snprintf(phrase, sizeof(phrase), ",B=%d %d %c %u",
+		(void)snprintf(phrase, sizeof(phrase), ",B=%d %u %c %u",
 		    (int)gpsd_get_speed(&sub->device->ttyset),
 			9 - sub->device->gpsdata.stopbits,
 			(int)sub->device->gpsdata.parity,
@@ -1205,6 +1212,7 @@ static void handle_control(int sfd, char *buf)
     struct gps_device_t	*chp;
     int cfd;
 
+    /*@ -sefparams @*/
     if (buf[0] == '-') {
 	p = snarfline(buf+1, &stash);
 	gpsd_report(LOG_INF, "<= control(%d): removing %s\n", sfd, stash);
@@ -1253,6 +1261,7 @@ static void handle_control(int sfd, char *buf)
 	    }
 	}
     }
+    /*@ +sefparams @*/
 }
 
 /*@ -mustfreefresh @*/
diff --git a/gpsd.h-tail b/gpsd.h-tail
index 7c0dfd03..fc156feb 100644
--- a/gpsd.h-tail
+++ b/gpsd.h-tail
@@ -390,8 +390,8 @@ extern void gpsd_close(struct gps_device_t *);
 
 extern void gpsd_zero_satellites(/*@out@*/struct gps_data_t *sp)/*@modifies sp@*/;
 extern void gpsd_interpret_subframe(struct gps_device_t *, unsigned int[]);
-extern /*@ observer @*/ char *gpsd_hexdump(const void *, size_t);
-extern /*@ observer @*/ char *gpsd_hexdump_wrapper(const void *, size_t, int);
+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 *, int);
 extern int hex2bin(char *);
 extern void ntpd_link_activate(struct gps_device_t *session);
@@ -436,7 +436,6 @@ void gpsd_report(int, const char *, ...);
 
 #ifdef S_SPLINT_S
 extern bool finite(double);
-extern int cfmakeraw(struct termios *);
 extern struct protoent *getprotobyname(const char *);
 extern /*@observer@*/char *strptime(const char *,const char *tp,/*@out@*/struct tm *)/*@modifies tp@*/;
 extern struct tm *gmtime_r(const time_t *,/*@out@*/struct tm *tp)/*@modifies tp@*/;
diff --git a/gpspipe.c b/gpspipe.c
index ae7dc95e..5da625d5 100644
--- a/gpspipe.c
+++ b/gpspipe.c
@@ -57,30 +57,32 @@ static void daemonize(void) {
   if (i>0) exit(0); /* parent exits */
 
   /* Obtain a new process group. */
-  setsid();
+  (void)setsid();
 
   /* Close all open descriptors. */
   for(i=getdtablesize();i>=0;--i)
-    close(i);
+      (void)close(i);
 
   /* Reopen STDIN, STDOUT, STDERR to /dev/null. */
   i=open("/dev/null",O_RDWR);	/* STDIN */
+  /*@ -sefparams @*/
   assert(dup(i) != -1); 	/* STDOUT */
   assert(dup(i) != -1);		/* STDERR */
 
   /* Know thy mask. */
-  umask(0x033);
+  (void)umask(0x033);
 
   /* Run from a known spot. */
   assert(chdir("/") != -1);
+  /*@ +sefparams @*/
 
   /* Catch child sig */
-  signal(SIGCHLD,SIG_IGN);
+  (void)signal(SIGCHLD,SIG_IGN);
 
- /* Ignore tty signals */
-  signal(SIGTSTP,SIG_IGN);
-  signal(SIGTTOU,SIG_IGN);
-  signal(SIGTTIN,SIG_IGN);
+  /* Ignore tty signals */
+  (void)signal(SIGTSTP,SIG_IGN);
+  (void)signal(SIGTTOU,SIG_IGN);
+  (void)signal(SIGTTIN,SIG_IGN);
 }
 
 /* open the serial port and set it up */
@@ -212,7 +214,7 @@ int main( int argc, char **argv)
 	exit(1);
     }
 
-    if (filename==NULL && daemon==true) {
+    if (filename==NULL && daemon) {
 	(void)fprintf(stderr, "gpsipipe: use of '-d' requires '-f'.\n");
 	exit(1);
     }
@@ -255,7 +257,7 @@ int main( int argc, char **argv)
 
     /* Sleep for ten seconds if the user requested it. */
     if (sleepy)
-      sleep(10);
+	(void)sleep(10);
 
     /* Open the output file if the user requested it.  If the user
        requested '-R', we use the 'b' flag in fopen() to "do the right
@@ -298,7 +300,7 @@ int main( int argc, char **argv)
 	exit(1);
     }
 
-    if ((isatty(STDERR_FILENO) == 0) || (daemon==true))
+    if ((isatty(STDERR_FILENO) == 0) || daemon)
 	vflag = 0;
 
     for(;;) {
diff --git a/gpsutils.c b/gpsutils.c
index 4bf4580e..e7b06d3f 100644
--- a/gpsutils.c
+++ b/gpsutils.c
@@ -178,7 +178,7 @@ double iso8601_to_unix(/*@in@*/char *isotime)
     struct tm tm;
 
     /*@i1@*/dp = strptime(isotime, "%Y-%m-%dT%H:%M:%S", &tm);
-    if (dp && *dp == '.')
+    if (dp != NULL && *dp == '.')
 	usec = strtod(dp, NULL);
     else
 	usec = 0;
diff --git a/italk.c b/italk.c
index 2815109d..a3791f67 100644
--- a/italk.c
+++ b/italk.c
@@ -114,7 +114,7 @@ static gps_mask_t decode_itk_prnstatus(struct gps_device_t *session, unsigned ch
     nchan = (unsigned int)((len - 10 - 52) / 20);
     nsv = 0;
     for (i = st = 0; i < nchan; i++) {
-	int off = 7+ 52 + 20 * i;
+	unsigned int off = 7+ 52 + 20 * i;
 	unsigned short flags;
 
 	flags = getleuw(buf, off);
diff --git a/libgps.c b/libgps.c
index 4ce3c5df..76a88bf2 100644
--- a/libgps.c
+++ b/libgps.c
@@ -282,20 +282,20 @@ static void gps_unpack(char *buf, struct gps_data_t *gpsdata)
 			gpsdata->set |= DEVICELIST_SET;
 		    }
 		    if (sp[2] != '?') {
+			/*@ -nullderef -nullpass -mustfreeonly -dependenttrans @*/
 			char *rc = strdup(sp);
-			sp = rc;
-			/*@ -nullderef @*/
-			gpsdata->ndevices = (int)strtol(sp+2, &sp, 10);
+			char *sp2 = rc;
+			gpsdata->ndevices = (int)strtol(sp2+2, &sp2, 10);
 			gpsdata->devicelist = (char **)calloc(
 			    (size_t)gpsdata->ndevices,
 			    sizeof(char **));
 			/*@ -nullstate -mustfreefresh @*/
-			gpsdata->devicelist[i=0] = strdup(strtok_r(sp+1, " \r\n", &ns));
-			while ((sp = strtok_r(NULL, " \r\n",  &ns)))
-			    gpsdata->devicelist[++i] = strdup(sp);
-			/*@ +nullstate +mustfreefresh @*/
-			/*@ +nullderef @*/
+			gpsdata->devicelist[i=0] = strdup(strtok_r(sp2+1, " \r\n", &ns));
+			while ((sp2 = strtok_r(NULL, " \r\n",  &ns)))
+			    gpsdata->devicelist[++i] = strdup(sp2);
 			free(rc);
+			/*@ +nullstate +mustfreefresh @*/
+			/*@ +nullderef +nullpass +dependenttrans +mustfreeonly @*/
 			gpsdata->set |= DEVICELIST_SET;
 		    }
 		    break;
@@ -560,7 +560,7 @@ int gps_query(struct gps_data_t *gpsdata, const char *fmt, ... )
 }
 
 #ifdef HAVE_LIBPTHREAD
-static void *poll_gpsd(void *args) 
+static /*@null@*/void *poll_gpsd(void *args) 
 /* helper for the thread launcher */
 {
     int oldtype, oldstate;
@@ -604,13 +604,16 @@ int gps_set_callback(struct gps_data_t *gpsdata,
 int gps_del_callback(struct gps_data_t *gpsdata, pthread_t *handler)
 /* delete asynchronous callback and kill its thread */
 {
+    /*@ -nullstate @*/
     int res;
+
     /*@i@*/res = pthread_cancel(*handler);	/* we cancel the whole thread */
-    pthread_join(*handler, NULL);	/* wait for thread to actually terminate */
+    /*@i1@*/pthread_join(*handler, NULL);	/* wait for thread to actually terminate */
     gpsdata->thread_hook = NULL;	/* finally we cancel the callback */
     if (res == 0) 			/* tell gpsd to stop sending data */
-	(void)gps_query(gpsdata,"w-\n");	/* disable watcher mode */
+	/*@i1@*/(void)gps_query(gpsdata,"w-\n");	/* disable watcher mode */
     return res;
+    /*@ +nullstate @*/
 }
 #endif /* HAVE_LIBPTHREAD */
 
diff --git a/libgpsd_core.c b/libgpsd_core.c
index 415acff5..a4f1d165 100644
--- a/libgpsd_core.c
+++ b/libgpsd_core.c
@@ -126,7 +126,7 @@ void gpsd_deactivate(struct gps_device_t *session)
 }
 
 #if defined(PPS_ENABLE) && defined(TIOCMIWAIT)
-static void *gpsd_ppsmonitor(void *arg)
+static /*@null@*/void *gpsd_ppsmonitor(void *arg)
 {
     struct gps_device_t *session = (struct gps_device_t *)arg;
     int cycle,duration, state = 0, laststate = -1, unchanged = 0;
diff --git a/nmea_parse.c b/nmea_parse.c
index cd5e4c8d..eda0e276 100644
--- a/nmea_parse.c
+++ b/nmea_parse.c
@@ -750,9 +750,10 @@ gps_mask_t nmea_parse(char *sentence, struct gps_device_t *session)
     typedef gps_mask_t (*nmea_decoder)(int count, char *f[], struct gps_device_t *session);
     static struct {
 	char *name;
-	int nf;		/* minimum number of fields required to parse */
+	int nf;			/* minimum number of fields required to parse */
 	nmea_decoder decoder;
     } nmea_phrase[] = {
+	/*@ -nullassign @*/
 	{"RMC", 8,	processGPRMC},
 	{"GGA", 13,	processGPGGA},
 	{"GLL", 7, 	processGPGLL},
@@ -773,6 +774,7 @@ gps_mask_t nmea_parse(char *sentence, struct gps_device_t *session)
 #ifdef OCEANSERVER_ENABLE
 	{"OHPR", 18,	processOHPR},
 #endif /* OCEANSERVER_ENABLE */
+	/*@ +nullassign @*/
     };
     volatile unsigned char buf[NMEA_MAX+1];
 
diff --git a/ntrip.c b/ntrip.c
index cac10251..0002df2b 100644
--- a/ntrip.c
+++ b/ntrip.c
@@ -43,7 +43,7 @@ struct ntrip_stream_t {
 static struct ntrip_stream_t ntrip_stream;
 
 /*@ -temptrans -mustfreefresh @*/
-static char *ntrip_field_iterate(char *start, /*@null@*/char *prev, const char *eol)
+static /*@null@*/char *ntrip_field_iterate(/*@null@*/char *start, /*@null@*/char *prev, const char *eol)
 {
     char *s, *t, *u;
 
@@ -292,7 +292,7 @@ static int ntrip_stream_probe(const char *caster,
 		   "Connection: close\r\n"
 		   "\r\n",
 		   VERSION);
-    if (write(dsock, buf, strlen(buf)) != strlen(buf)) {
+    if (write(dsock, buf, strlen(buf)) != (ssize_t)strlen(buf)) {
 	    printf("ntrip stream write error %d\n", dsock);
 	    return -1;
     }
@@ -326,7 +326,7 @@ static int ntrip_auth_encode(const struct ntrip_stream_t *stream,
 /*@ -nullpass @*/ /* work around a splint bug */
 static int ntrip_stream_open(const char *caster,
 			     const char *port,
-			     const char *auth,
+			     /*@null@*/const char *auth,
 			     struct gps_context_t *context, 
 			     struct ntrip_stream_t *stream)
 {
@@ -350,7 +350,7 @@ static int ntrip_stream_open(const char *caster,
 		   "Connection: close\r\n"
 		   "\r\n",
 		   stream->mountpoint, VERSION, authstr);
-    if (write(context->dsock, buf, strlen(buf)) != strlen(buf)) {
+    if (write(context->dsock, buf, strlen(buf)) != (ssize_t)strlen(buf)) {
 	    printf("ntrip stream write error on %d\n", context->dsock);
 	    return -1;
     }
@@ -463,7 +463,7 @@ void ntrip_report(struct gps_device_t *session)
 	if (session->context->dsock > -1) {
 	    char buf[BUFSIZ];
 	    gpsd_position_fix_dump(session, buf, sizeof(buf));
-	    if (write(session->context->dsock, buf, strlen(buf)) == strlen(buf))
+	    if (write(session->context->dsock, buf, strlen(buf)) == (ssize_t)strlen(buf))
 		gpsd_report(LOG_IO, "=> dgps %s", buf);
 	    else
 		gpsd_report(LOG_IO, "ntrip report write failed", buf);
diff --git a/rtcm2.c b/rtcm2.c
index f5884eff..7de646e8 100644
--- a/rtcm2.c
+++ b/rtcm2.c
@@ -705,11 +705,12 @@ int rtcm2_undump(/*@out@*/struct rtcm2_t *rtcmp, char *buf)
 	if (n >= DIMENSION(rtcmp->msg_data.words))
 	    return 0;
 	else {
-	    fldcount = sscanf(buf, "U\t0x%08x\n", &v);
+	    unsigned int u;
+	    fldcount = sscanf(buf, "U\t0x%08x\n", &u);
 	    if (fldcount != 1)
 		return (int)(-rtcmp->type-1);
 	    else {
-		rtcmp->msg_data.words[n] = (isgps30bits_t)v;
+		rtcmp->msg_data.words[n] = (isgps30bits_t)u;
 		if (n == rtcmp->length-1)
 		    return 0;
 		else
diff --git a/rtcm3.c b/rtcm3.c
index 117f148c..78387761 100644
--- a/rtcm3.c
+++ b/rtcm3.c
@@ -51,6 +51,8 @@ firmware.
 /* Other magic values */
 #define INVALID_PSEUDORANGE		0x80000	/* DF012 */
 
+/*@ -type @*/	/* re-enable when we're ready to take this live */
+
 void rtcm3_unpack(/*@out@*/struct rtcm3_t *rtcm, char *buf)
 /* break out the raw bits into the scaled report-structure fields */
 {
@@ -100,7 +102,7 @@ void rtcm3_unpack(/*@out@*/struct rtcm3_t *rtcm, char *buf)
 	    rtcm->rtcmtypes.rtcm3_1002.header.satcount   = (ushort)ugrab(5);
 	    rtcm->rtcmtypes.rtcm3_1002.header.smoothing  = (bool)ugrab(1);
 	    rtcm->rtcmtypes.rtcm3_1002.header.interval   = (ushort)ugrab(3);
-	    for (i = 0; i < rtcm->rtcmtypes.rtcm3_1001.header.satcount; i++) {
+	    for (i = 0; i < rtcm->rtcmtypes.rtcm3_1002.header.satcount; i++) {
 		rtcm->rtcmtypes.rtcm3_1002.rtk_data[i].ident = (ushort)ugrab(6);
 		rtcm->rtcmtypes.rtcm3_1002.rtk_data[i].L1.indicator = (unsigned char)ugrab(1);
 		temp = (long)sgrab(24);
@@ -126,7 +128,7 @@ void rtcm3_unpack(/*@out@*/struct rtcm3_t *rtcm, char *buf)
 	    rtcm->rtcmtypes.rtcm3_1003.header.satcount   = (ushort)ugrab(5);
 	    rtcm->rtcmtypes.rtcm3_1003.header.smoothing  = (bool)ugrab(1);
 	    rtcm->rtcmtypes.rtcm3_1003.header.interval   = (ushort)ugrab(3);
-	    for (i = 0; i < rtcm->rtcmtypes.rtcm3_1001.header.satcount; i++) {
+	    for (i = 0; i < rtcm->rtcmtypes.rtcm3_1003.header.satcount; i++) {
 		rtcm->rtcmtypes.rtcm3_1003.rtk_data[i].ident = (ushort)ugrab(6);
 		rtcm->rtcmtypes.rtcm3_1003.rtk_data[i].L1.indicator = (unsigned char)ugrab(1);
 		temp = (long)sgrab(24);
@@ -161,7 +163,7 @@ void rtcm3_unpack(/*@out@*/struct rtcm3_t *rtcm, char *buf)
 	    rtcm->rtcmtypes.rtcm3_1004.header.satcount   = (ushort)ugrab(5);
 	    rtcm->rtcmtypes.rtcm3_1004.header.smoothing  = (bool)ugrab(1);
 	    rtcm->rtcmtypes.rtcm3_1004.header.interval   = (ushort)ugrab(3);
-	    for (i = 0; i < rtcm->rtcmtypes.rtcm3_1001.header.satcount; i++) {
+	    for (i = 0; i < rtcm->rtcmtypes.rtcm3_1004.header.satcount; i++) {
 		rtcm->rtcmtypes.rtcm3_1004.rtk_data[i].ident = (ushort)ugrab(6);
 		rtcm->rtcmtypes.rtcm3_1004.rtk_data[i].L1.indicator = (bool)ugrab(1);
 		temp = (long)sgrab(24);
@@ -464,4 +466,6 @@ void rtcm3_dump(struct rtcm3_t *rtcm, FILE *fp)
 #undef BOOL
 }
 
+/*@ +type @*/
+
 #endif /* RTCM104V3_ENABLE */
diff --git a/rtcmdecode.c b/rtcmdecode.c
index 75b960f2..0b27e273 100644
--- a/rtcmdecode.c
+++ b/rtcmdecode.c
@@ -110,8 +110,8 @@ static void encode(FILE *fpin, FILE *fpout)
 	    (void)memset(lexer.isgps.buf, 0, sizeof(lexer.isgps.buf));
 	    (void)rtcm2_repack(&rtcm, lexer.isgps.buf);
 	    if (fwrite(lexer.isgps.buf, 
-			 sizeof(isgps30bits_t), 
-		       (size_t)rtcm.length, fpout) <= 0)
+		       sizeof(isgps30bits_t), 
+		       (size_t)rtcm.length, fpout) != (size_t)rtcm.length)
 		(void) fprintf(stderr, "rtcmdecode: report write failed.\n");
 	    memset(&lexer, 0, sizeof(lexer));
 	} else if (status < 0) {
diff --git a/serial.c b/serial.c
index b937f513..1bd6f48a 100644
--- a/serial.c
+++ b/serial.c
@@ -208,14 +208,14 @@ int gpsd_open(struct gps_device_t *session)
     struct stat sb;
     mode_t mode = (mode_t)O_RDWR;
 
-    /*@ -boolops @*/
+    /*@ -boolops -type @*/
     if (session->context->readonly || ((stat(session->gpsdata.gps_device, &sb) != -1) && ((sb.st_mode & S_IFCHR) != S_IFCHR))){
 	mode = (mode_t)O_RDONLY;
 	gpsd_report(LOG_INF, "opening read-only GPS data source at '%s'\n", session->gpsdata.gps_device);
     } else {
 	gpsd_report(LOG_INF, "opening GPS data source at '%s'\n", session->gpsdata.gps_device);
     }
-    /*@ +boolops @*/
+    /*@ +boolops +type @*/
 
     if ((session->gpsdata.gps_fd = open(session->gpsdata.gps_device, (int)(mode|O_NONBLOCK|O_NOCTTY))) < 0) {
 	gpsd_report(LOG_ERROR, "device open failed: %s - retrying read-only\n", strerror(errno));
diff --git a/sirf.c b/sirf.c
index 4f4ed922..b0a617cc 100644
--- a/sirf.c
+++ b/sirf.c
@@ -440,7 +440,7 @@ static gps_mask_t sirf_msg_geodetic(struct gps_device_t *session, unsigned char
 
     session->gpsdata.fix.latitude = getbesl(buf, 23)*1e-7;
     session->gpsdata.fix.longitude = getbesl(buf, 27)*1e-7;
-    if (session->gpsdata.fix.latitude && session->gpsdata.fix.latitude)
+    if (session->gpsdata.fix.latitude!=0 && session->gpsdata.fix.latitude!=0)
 	mask |= LATLON_SET;
 
     if ((session->gpsdata.fix.eph =  getbesl(buf, 50)*1e-2) > 0)
@@ -451,7 +451,7 @@ static gps_mask_t sirf_msg_geodetic(struct gps_device_t *session, unsigned char
 	mask |= SPEEDERR_SET;
 
     /* HDOP should be available at byte 89, but in 231 it's zero. */
-    if ((session->gpsdata.hdop = getub(buf, 89) * 0.2) > 0)
+    if ((session->gpsdata.hdop = (unsigned int)getub(buf, 89) * 0.2) > 0)
 	mask |= HDOP_SET;
 
     if (session->driver.sirf.driverstate & SIRF_GE_232) {
diff --git a/sirfmon.c b/sirfmon.c
index 71900b4a..2bc2c4be 100644
--- a/sirfmon.c
+++ b/sirfmon.c
@@ -639,7 +639,7 @@ static int set_speed(unsigned int speed, unsigned int stopbits)
 	return NO_PACKET;
     (void)tcflush(devicefd, TCIOFLUSH);
 
-    (void)fprintf(stderr, "Hunting at speed %u, %dN%u\n",
+    (void)fprintf(stderr, "Hunting at speed %u, %uN%u\n",
 	    get_speed(&ttyset), 9-stopbits, stopbits);
 
     /* sniff for NMEA or SiRF packet */
@@ -814,7 +814,7 @@ static int readpkt(unsigned char *buf, size_t buflen)
 	return EOF;
 
     if (logfile != NULL) {
-	/*@ -shiftimplementation @*/
+	/*@ -shiftimplementation -sefparams +charint @*/
 	char outbuf[BUFSIZ];
 	(void)memcpy(outbuf, "\xa0\xa2", 2);
 	outbuf[2] = (len >> 8);
@@ -823,8 +823,8 @@ static int readpkt(unsigned char *buf, size_t buflen)
 	outbuf[4+len] = (csum >> 8);
 	outbuf[5+len] = (csum & 0xff);
 	(void)memcpy(outbuf+6+len, "\xb0\xb3", 2);
-	assert(fwrite(outbuf, sizeof(char), len+8, logfile) >= 1);
-	/*@ +shiftimplementation @*/
+	assert(fwrite(outbuf, sizeof(char), (size_t)len+8, logfile) >= 1);
+	/*@ +shiftimplementation +sefparams -charint @*/
     }
     return len;
 }
@@ -859,14 +859,18 @@ static bool sendpkt(unsigned char *buf, size_t len, char *device)
 	return false;
     else {
 	if (!serial) {
+	    /*@ -sefparams @*/
 	    assert(write(controlfd, "!", 1) != -1);
 	    assert(write(controlfd, device, strlen(device)) != -1);
 	    assert(write(controlfd, "=", 1) != -1);
+	    /*@ +sefparams @*/
 	}
 	st = write(controlfd, buf,len);
 	if (!serial)
 	    /* enough room for "ERROR\r\n\0" */
+	    /*@ -sefparams @*/
 	    assert(read(controlfd, buf, 8) != -1);
+	    /*@ +sefparams @*/
 	return ((size_t)st == len);
     }
 }
@@ -925,7 +929,7 @@ static void command(char buf[], size_t len, const char *fmt, ... )
     (void)vsnprintf(buf, len, fmt, ap);
     va_end(ap);
 
-    assert(write(devicefd, buf, strlen(buf)) != -1);
+    /*@i1@*/assert(write(devicefd, buf, strlen(buf)) != -1);
     n = read(devicefd, buf, len);
     if (n >= 0) {
 	buf[n] = '\0';
@@ -991,12 +995,13 @@ int main (int argc, char **argv)
 	    }
 	}
     }
-    /*@ +nullpass +branchstate @*/
 
     /*@ -boolops */
     if (!arg || (arg && !slash) || (arg && colon1 && slash)) {	
 	if (!server)
 	    server = "127.0.0.1";
+	if (!port)
+	    port = DEFAULT_GPSD_PORT;
 	devicefd = netlib_connectsock(server, port, "tcp");
 	if (devicefd < 0) {
 	    (void)fprintf(stderr, 
@@ -1020,6 +1025,7 @@ int main (int argc, char **argv)
 	serial = true;
     }
     /*@ +boolops */
+    /*@ +nullpass +branchstate @*/
 
     /* quit cleanly if an assertion fails */
     (void)signal(SIGABRT, onsig);
@@ -1270,9 +1276,11 @@ int main (int argc, char **argv)
 		    display(cmdwin, 1, 0, "%s %d N %d", device,bps,stopbits);
 		} else {
 		    line[0] = 'b';
+		    /*@ -sefparams @*/
 		    assert(write(devicefd, line, strlen(line)) != -1);
 		    /* discard response */
 		    assert(read(devicefd, buf, sizeof(buf)) != -1);
+		    /*@ +sefparams @*/
 		}
 		break;
 
diff --git a/tsip.c b/tsip.c
index 30ddfc3a..8d182261 100644
--- a/tsip.c
+++ b/tsip.c
@@ -19,7 +19,7 @@
 #ifdef TSIP_ENABLE
 #define TSIP_CHANNELS	12
 
-static int tsip_write(int fd, unsigned int id, unsigned char *buf, size_t len)
+static int tsip_write(int fd, unsigned int id, /*@null@*/unsigned char *buf, size_t len)
 {
 #ifdef ALLOW_RECONFIGURE
     char buf2[BUFSIZ];
@@ -33,6 +33,7 @@ static int tsip_write(int fd, unsigned int id, unsigned char *buf, size_t len)
     if (write(fd,buf2,2) != 2)
 	return -1;
 
+    /*@ -nullderef @*/
     while (len-- > 0) {
 	if (*buf == '\x10')
 	    if (write(fd,buf2,1) != 1)
@@ -41,6 +42,7 @@ static int tsip_write(int fd, unsigned int id, unsigned char *buf, size_t len)
 	if (write(fd,buf++,1) != 1)
 	    return -1;
     }
+    /*@ +nullderef @*/
 
     buf2[1] = '\x03';
     /*@ -charint @*/
diff --git a/ubx.c b/ubx.c
index 59e58c20..b807e823 100644
--- a/ubx.c
+++ b/ubx.c
@@ -36,7 +36,7 @@ static bool have_port_configuration = false;
 static unsigned char original_port_settings[20];
 static unsigned char sbas_in_use;
 
-	bool 		ubx_write(int fd, unsigned char msg_class, unsigned char msg_id, unsigned char *msg, unsigned short data_len);
+	bool 		ubx_write(int fd, unsigned int msg_class, unsigned int msg_id, unsigned char *msg, unsigned short data_len);
 	gps_mask_t 	ubx_parse(struct gps_device_t *session, unsigned char *buf, size_t len);
 	void 		ubx_catch_model(struct gps_device_t *session, unsigned char *buf, size_t len);
 static	gps_mask_t 	ubx_msg_nav_sol(struct gps_device_t *session, unsigned char *buf, size_t data_len);
@@ -413,7 +413,7 @@ gps_mask_t ubx_parse(struct gps_device_t *session, unsigned char *buf, size_t le
 	    for(i=6;i<26;i++)
 		original_port_settings[i-6] = buf[i];				/* copy the original port settings */
 	    buf[14+6] &= ~0x02;							/* turn off NMEA output on this port */
-	    ubx_write(session->gpsdata.gps_fd, 0x06, 0x00, &buf[6], 20);	/* send back with all other settings intact */
+	    (void)ubx_write(session->gpsdata.gps_fd, 0x06, 0x00, &buf[6], 20);	/* send back with all other settings intact */
 	    have_port_configuration = true;
 	    break;
 
@@ -472,7 +472,7 @@ void ubx_catch_model(struct gps_device_t *session, unsigned char *buf, size_t le
     }
 }
 
-bool ubx_write(int fd, unsigned char msg_class, unsigned char msg_id, unsigned char *msg, unsigned short data_len) {
+bool ubx_write(int fd, unsigned int msg_class, unsigned int msg_id, unsigned char *msg, unsigned short data_len) {
    unsigned char CK_A, CK_B;
    unsigned char head_tail[8];
    unsigned int i, count;
@@ -526,8 +526,9 @@ static void ubx_configure(struct gps_device_t *session, unsigned int seq)
 
     gpsd_report(LOG_IO, "UBX configure: %d\n",seq);
 
-    ubx_write(session->gpsdata.gps_fd, 0x06, 0x00, NULL, 0);	/* get This port's settings */
+    (void)ubx_write(session->gpsdata.gps_fd, 0x06u, 0x00, NULL, 0);	/* get this port's settings */
 
+    /*@ -type @*/
     msg[0] = 0x03; /* SBAS mode enabled, accept testbed mode */
     msg[1] = 0x07; /* SBAS usage: range, differential corrections and integrity */
     msg[2] = 0x03; /* use the maximun search range: 3 channels */
@@ -536,42 +537,45 @@ static void ubx_configure(struct gps_device_t *session, unsigned int seq)
     msg[5] = 0x00;
     msg[6] = 0x00;
     msg[7] = 0x00;
-    ubx_write(session->gpsdata.gps_fd, 0x06, 0x16, msg, 8);
+    (void)ubx_write(session->gpsdata.gps_fd, 0x06u, 0x16, msg, 8);
 
     msg[0] = 0x01; /* class */
     msg[1] = 0x04; /* msg id  = UBX_NAV_DOP */
     msg[2] = 0x01; /* rate */
-    ubx_write(session->gpsdata.gps_fd, 0x06, 0x01, msg, 3);
+    (void)ubx_write(session->gpsdata.gps_fd, 0x06u, 0x01, msg, 3);
     msg[0] = 0x01; /* class */
     msg[1] = 0x06; /* msg id  = NAV-SOL */
     msg[2] = 0x01; /* rate */
-    ubx_write(session->gpsdata.gps_fd, 0x06, 0x01, msg, 3);
+    (void)ubx_write(session->gpsdata.gps_fd, 0x06u, 0x01, msg, 3);
     msg[0] = 0x01; /* class */
     msg[1] = 0x20; /* msg id  = UBX_NAV_TIMEGPS */
     msg[2] = 0x01; /* rate */
-    ubx_write(session->gpsdata.gps_fd, 0x06, 0x01, msg, 3);
+    (void)ubx_write(session->gpsdata.gps_fd, 0x06u, 0x01, msg, 3);
     msg[0] = 0x01; /* class */
     msg[1] = 0x30; /* msg id  = NAV-SVINFO */
     msg[2] = 0x0a; /* rate */
-    ubx_write(session->gpsdata.gps_fd, 0x06, 0x01, msg, 3);
+    (void)ubx_write(session->gpsdata.gps_fd, 0x06u, 0x01, msg, 3);
     msg[0] = 0x01; /* class */
     msg[1] = 0x32; /* msg id  = NAV-SBAS */
     msg[2] = 0x0a; /* rate */
-    ubx_write(session->gpsdata.gps_fd, 0x06, 0x01, msg, 3);
+    (void)ubx_write(session->gpsdata.gps_fd, 0x06u, 0x01, msg, 3);
+    /*@ +type @*/
 
 }
 
 static void ubx_revert(struct gps_device_t *session)
 {
+    /*@ -type @*/
     unsigned char msg[4] = {
 	0x00, 0x00,	/* hotstart */
 	0x01,		/* controlled software reset */
 	0x00};		/* reserved */
+    /*@ +type @*/
 
     gpsd_report(LOG_IO, "UBX revert\n");
 
-/* Reverting all in one fast and reliable reset */
-    ubx_write(session->gpsdata.gps_fd, 0x06, 0x04, msg, 4); /* CFG-RST */
+    /* Reverting all in one fast and reliable reset */
+    (void)ubx_write(session->gpsdata.gps_fd, 0x06, 0x04, msg, 4); /* CFG-RST */
 }
 #endif /* ALLOW_RECONFIGURE */
 
@@ -583,6 +587,7 @@ static void ubx_nmea_mode(struct gps_device_t *session, int mode)
     if(!have_port_configuration)
 	return;
 
+    /*@ +charint @*/
     for(i=0;i<22;i++)
 	buf[i] = original_port_settings[i];	/* copy the original port settings */
     if(buf[0] == 0x01)				/* set baudrate on serial port only */
@@ -595,7 +600,8 @@ static void ubx_nmea_mode(struct gps_device_t *session, int mode)
 	buf[14] &= ~0x02;			/* turn off NMEA output on this port */
 	buf[14] |=  0x01;			/* turn on UBX output on this port */
     }
-    ubx_write(session->gpsdata.gps_fd, 0x06, 0x00, &buf[6], 20);	/* send back with all other settings intact */
+    /*@ -charint @*/
+    (void)ubx_write(session->gpsdata.gps_fd, 0x06u, 0x00, &buf[6], 20);	/* send back with all other settings intact */
 }
 
 static bool ubx_speed(struct gps_device_t *session, speed_t speed)
@@ -609,7 +615,7 @@ static bool ubx_speed(struct gps_device_t *session, speed_t speed)
     for(i=0;i<22;i++)
 	buf[i] = original_port_settings[i];	/* copy the original port settings */
     putlelong(buf, 8, speed);
-    ubx_write(session->gpsdata.gps_fd, 0x06, 0x00, &buf[6], 20);	/* send back with all other settings intact */
+    (void)ubx_write(session->gpsdata.gps_fd, 0x06, 0x00, &buf[6], 20);	/* send back with all other settings intact */
     return true;
 }
 
diff --git a/xgpsspeed.c b/xgpsspeed.c
index 8aecaafe..783e4b5d 100644
--- a/xgpsspeed.c
+++ b/xgpsspeed.c
@@ -153,7 +153,7 @@ int main(int argc, char **argv)
     else 
         (void)XtSetArg(args[0], XtNlabel, "Knots");
 
-    /*@ +immediatetrans +usedef +observertrans +statictrans @*/
+    /*@ +immediatetrans +usedef +observertrans +statictrans -compmempass @*/
     (void)XtCreateManagedWidget("name", labelWidgetClass, base, args, 1);
     
     /**** Tachometer widget ****/