diff options
| -rw-r--r-- | gpsd.c | 35 | ||||
| -rw-r--r-- | gpsd_json.c | 6 | ||||
| -rw-r--r-- | json.c | 20 | ||||
| -rw-r--r-- | libgps.c | 19 |
4 files changed, 54 insertions, 26 deletions
@@ -747,6 +747,7 @@ static /*@null@*/struct channel_t *assign_channel(struct subscriber_t *user, gnss_type type, /*@null@*/struct gps_device_t *forcedev) { + /*@-temptrans@*/ struct channel_t *chp, *channel; bool was_unassigned; @@ -880,6 +881,7 @@ static /*@null@*/struct channel_t *assign_channel(struct subscriber_t *user, channel->subscriber = user; return channel; + /*@+temptrans@*/ } /*@ +branchstate +usedef +globstate @*/ @@ -1058,6 +1060,14 @@ static /*@null@*/struct channel_t *mandatory_assign_channel(struct subscriber_t return channel; } +/* + * After each channel assignment, it must be the case that eother the + * the turned channel pointer is null or points to a channel block with + * a nonzero device field. The dataflow analysis splint does is not + * quite good enough to catch this, alas, so we need to temporarily + * disable its null-dereference check. + */ +/*@ -nullderef -nullpass -mustfreefresh @*/ static bool handle_oldstyle(struct subscriber_t *sub, char *buf, /*@out@*/char *reply, size_t replylen) /* interpret a client request; cfd is the socket back to the client */ @@ -1070,15 +1080,6 @@ static bool handle_oldstyle(struct subscriber_t *sub, char *buf, sub->new_style_responses = false; #endif /* defined(OLDSTYLE_ENABLE) && defined(GPSDNG_ENABLE) */ - /* - * After each channel assignment, it must be the case that eother the - * the turned channel pointer is null or points to a channel block with - * a nonzero device field. The dataflow analysis splint does is not - * quite good enough to catch this, alas, so we need to temporarily - * disable its null-dereference check. - */ - /*@ -nullderef -nullpass @*/ - (void)strlcpy(reply, "GPSD", replylen); replylen -= 4; p = buf; @@ -1616,9 +1617,9 @@ static bool handle_oldstyle(struct subscriber_t *sub, char *buf, } breakout: (void)strlcat(reply, "\r\n", replylen); - /*@ +nullderef +nullpass @*/ return true; } +/*@ +nullderef +nullpass +mustfreefresh @*/ #endif /* OLDSTYLE_ENABLE */ #ifdef GPSDNG_ENABLE @@ -1645,7 +1646,7 @@ static void handle_newstyle_request(struct subscriber_t *sub, { struct gps_device_t *devp; struct channel_t *channel; - const char *end; + const char *end = NULL; #if defined(OLDSTYLE_ENABLE) && defined(GPSDNG_ENABLE) sub->new_style_responses = true; @@ -1658,6 +1659,11 @@ static void handle_newstyle_request(struct subscriber_t *sub, * declare it @null@ and use -compdef around the JSON reader calls. */ /*@-compdef@*/ + /* + * See above... + */ + /*@-nullderef -nullpass@*/ + /* * Still to be implemented: equivalents of Z $ @@ -1709,6 +1715,7 @@ static void handle_newstyle_request(struct subscriber_t *sub, buf = end; } channel = NULL; + /*@-branchstate@*/ if (status != 0) { (void)snprintf(reply, replylen, "{\"class\":ERROR\",\"message\":\"Invalid DEVICE: %s\"}\r\n", @@ -1765,6 +1772,7 @@ static void handle_newstyle_request(struct subscriber_t *sub, } } } + /*@+branchstate@*/ } /* dump a response for each selected channel */ for (channel = channels; channel < channels + NITEMS(channels); channel++) @@ -1792,6 +1800,7 @@ static void handle_newstyle_request(struct subscriber_t *sub, } bailout: *after = buf; + /*@+nullderef +nullpass@*/ /*@+compdef@*/ } #endif /* GPSDNG_ENABLE */ @@ -2232,6 +2241,7 @@ int main(int argc, char *argv[]) #endif /* GPSDNG_ENABLE */ } /* copy/merge device data into subscriber fix buffers */ + /*@-nullderef -nullpass@*/ for (channel = channels; channel < channels + NITEMS(channels); channel++) { @@ -2250,6 +2260,7 @@ int main(int argc, char *argv[]) &channel->fixbuffer, &channel->oldfix); } } + /*@+nullderef -nullpass@*/ } /* copy each RTCM-104 correction to all GPSes */ if ((changed & RTCM2_SET) != 0 || (changed & RTCM3_SET) != 0) { @@ -2264,6 +2275,7 @@ int main(int argc, char *argv[]) for (channel = channels; channel < channels + NITEMS(channels); channel++) { sub = channel->subscriber; /* some listeners may be in watcher mode */ + /*@-nullderef@*/ if (sub != NULL && sub->policy.watcher) { char buf2[BUFSIZ]; int state = channel->device->cycle_state; @@ -2346,6 +2358,7 @@ int main(int argc, char *argv[]) #endif /* GPSDNG_ENABLE */ } } + /*@-nullderef@*/ } } diff --git a/gpsd_json.c b/gpsd_json.c index 55c77d2b..03cf9291 100644 --- a/gpsd_json.c +++ b/gpsd_json.c @@ -22,6 +22,7 @@ representations to gpsd core strctures, and vice_versa. char *json_stringify(/*@out@*/char *to, size_t len, /*@in@*/const char *from) /* escape double quotes and control characters inside a JSON string */ { + /*@-temptrans@*/ const char *sp; char *tp; @@ -64,6 +65,7 @@ char *json_stringify(/*@out@*/char *to, size_t len, /*@in@*/const char *from) *tp = '\0'; return to; + /*@+temptrans@*/ } void json_version_dump(/*@out@*/char *reply, size_t replylen) @@ -247,6 +249,7 @@ void json_device_dump(const struct gps_device_t *device, replylen); (void)strlcat(reply, "\",", replylen); } + /*@-mustfreefresh@*/ if (device->subtype[0] != '\0') { (void)strlcat(reply, "\"subtype\":\",", replylen); (void)strlcat(reply, @@ -254,6 +257,7 @@ void json_device_dump(const struct gps_device_t *device, replylen); (void)strlcat(reply, "\",", replylen); } + /*@+mustfreefresh@*/ (void)snprintf(reply+strlen(reply), replylen-strlen(reply), "\"native\":%d,\"bps\":%d,\"parity\":\"%c\",\"stopbits\":%u,\"cycle\":%2.2f", device->gpsdata.dev.driver_mode, @@ -274,12 +278,14 @@ void json_device_dump(const struct gps_device_t *device, void json_watch_dump(const struct policy_t *ccp, /*@out@*/char *reply, size_t replylen) { + /*@-compdef@*/ (void)snprintf(reply+strlen(reply), replylen-strlen(reply), "{\"class\":\"WATCH\",\"enable\":%s,\"raw\":%d,\"buffer_policy\":%d,\"scaled\":%s}\r\n", ccp->watcher ? "true" : "false", ccp->raw, ccp->buffer_policy, ccp->scaled ? "true" : "false"); + /*@+compdef@*/ } #if defined(RTCM104V2_ENABLE) @@ -62,6 +62,7 @@ has to be inline in the struct. # define json_debug_trace(args) /*@i1@*/do { } while (0) #endif /* JSONDEBUG */ +/*@-immediatetrans -dependenttrans -usereleased -compdef@*/ static /*@null@*/char *json_target_address(const struct json_attr_t *cursor, /*@null@*/const struct json_array_t *parent, int offset) @@ -90,14 +91,15 @@ static /*@null@*/char *json_target_address(const struct json_attr_t *cursor, /* tricky case - hacking a member in an array of structures */ return parent->arr.objects.base + (offset * parent->arr.objects.stride) + cursor->addr.offset; } +/*@-immediatetrans -dependenttrans +usereleased +compdef@*/ static int json_internal_read_object(const char *cp, const struct json_attr_t *attrs, - const struct json_array_t *parent, + /*@null@*/const struct json_array_t *parent, int offset, /*@null@*/const char **end) { - /*@ -nullstate -nullderef -mustfreefresh @*/ + /*@ -nullstate -nullderef -mustfreefresh -nullpass -usedef @*/ enum {init, await_attr, in_attr, await_value, in_val_string, in_escape, in_val_token, post_val} state = 0; #ifdef JSONDEBUG @@ -116,6 +118,12 @@ static int json_internal_read_object(const char *cp, const struct json_enum_t *mp; char *lptr; +#ifdef S_SPLINT_S + /* prevents gripes about buffers not being completely defined */ + memset(valbuf, '\0', sizeof(valbuf)); + memset(attrbuf, '\0', sizeof(attrbuf)); +#endif /* S_SPLINT_S */ + if (end != NULL) *end = NULL; /* give it a well-defined value on parse failure */ @@ -123,7 +131,6 @@ static int json_internal_read_object(const char *cp, for (cursor = attrs; cursor->attribute != NULL; cursor++) if (!cursor->nodefault) { lptr = json_target_address(cursor, parent, offset); - /*@-nullderef@*/ switch(cursor->type) { case integer: @@ -156,7 +163,6 @@ static int json_internal_read_object(const char *cp, case check: break; } - /*@+nullderef@*/ } json_debug_trace(("JSON parse begins.\n")); @@ -316,7 +322,6 @@ static int json_internal_read_object(const char *cp, (void)snprintf(valbuf, sizeof(valbuf), "%d", mp->value); } lptr = json_target_address(cursor, parent, offset); - /*@-nullderef@*/ switch(cursor->type) { case integer: @@ -353,7 +358,6 @@ static int json_internal_read_object(const char *cp, } break; } - /*@+nullderef@*/ if (isspace(*cp)) continue; else if (*cp == ',') @@ -374,11 +378,12 @@ good_parse: *end = cp; json_debug_trace(("JSON parse ends.\n")); return 0; - /*@ +nullstate +nullderef +mustfreefresh @*/ + /*@ +nullstate +nullderef +mustfreefresh +nullpass +usedef @*/ } int json_read_array(const char *cp, const struct json_array_t *arr, const char **end) { + /*@-nullstate -onlytrans@*/ int substatus, offset; char *tp; @@ -462,6 +467,7 @@ breakout: *end = cp; json_debug_trace(("leaving json_read_array() with %d elements\n", *arr->count)); return 0; + /*@+nullstate +onlytrans@*/ } int json_read_object(const char *cp, @@ -62,7 +62,7 @@ void gps_set_raw_hook(struct gps_data_t *gpsdata, gpsdata->raw_hook = hook; } -/*@ -branchstate -usereleased -mustfreefresh @*/ +/*@ -branchstate -usereleased -mustfreefresh -nullstate@*/ int gps_unpack(char *buf, struct gps_data_t *gpsdata) /* unpack a gpsd response into a status structure, buf must be writeable */ { @@ -194,24 +194,27 @@ int gps_unpack(char *buf, struct gps_data_t *gpsdata) /*@ +mustfreeonly */ break; case 'K': + /*@ -nullpass -mustfreeonly -dependenttrans@*/ if (sp[2] != '?') { char *rc = strdup(sp); char *sp2 = rc; char *ns2 = ns; memset(&gpsdata->devices, '\0', sizeof(gpsdata->devices)); gpsdata->devices.ndevices = (int)strtol(sp2+2, &sp2, 10); - (void)strlcpy(gpsdata->devices.list[i=0].path, + (void)strlcpy(gpsdata->devices.list[0].path, strtok_r(sp2+1," \r\n", &ns2), - sizeof(gpsdata->devices.list[i=0].path)); - while ((sp2 = strtok_r(NULL, " \r\n", &ns2))) + sizeof(gpsdata->devices.list[0].path)); + i = 0; + while ((sp2 = strtok_r(NULL, " \r\n", &ns2))!=NULL) if (i < MAXDEVICES_PER_USER-1) (void)strlcpy(gpsdata->devices.list[++i].path, sp2, - sizeof(gpsdata->devices.list[i=0].path)); + sizeof(gpsdata->devices.list[0].path)); free(rc); gpsdata->set |= DEVICELIST_SET; gpsdata->devices.time = timestamp(); } + /*@ +nullpass +mustfreeonly +dependenttrans@*/ break; case 'M': if (sp[2] == '?') { @@ -431,7 +434,7 @@ int gps_unpack(char *buf, struct gps_data_t *gpsdata) } #endif /* GPSDNG_ENABLE */ -/*@ -nullstate -compdef @*/ +/*@ -compdef @*/ if (gpsdata->raw_hook) gpsdata->raw_hook(gpsdata, buf, strlen(buf), 1); if (gpsdata->thread_hook) @@ -439,8 +442,8 @@ int gps_unpack(char *buf, struct gps_data_t *gpsdata) return 0; } -/*@ +nullstate +compdef @*/ -/*@ -branchstate +usereleased +mustfreefresh @*/ +/*@ +compdef @*/ +/*@ -branchstate +usereleased +mustfreefresh +nullstate@*/ /* * return: 0, success |