From b735d05e0579c60c542f7c8fcab961ce4401c32f Mon Sep 17 00:00:00 2001 From: "Eric S. Raymond" Date: Thu, 10 Sep 2009 11:09:03 +0000 Subject: Splint Cleanup Meets Billy The Kid. All regression tests pass. --- ais_json.c | 12 +++-- gps_json.h | 17 ++++--- gpsd.c | 13 ++++- gpsd_json.c | 152 +++++++++++++++++++++++++++++---------------------------- json.c | 23 ++++++--- json.h | 4 +- libgps.c | 2 +- libgps_json.c | 21 ++++++-- libgpsd_core.c | 2 +- rtcm2_json.c | 10 +++- 10 files changed, 151 insertions(+), 105 deletions(-) diff --git a/ais_json.c b/ais_json.c index 79ead5aa..d2f9c552 100644 --- a/ais_json.c +++ b/ais_json.c @@ -33,10 +33,12 @@ static void lenhex_unpack(const char *from, /*@ +mustdefine @*/ int json_ais_read(const char *buf, - char *path, size_t pathlen, - struct ais_t *ais, - const char **endptr) + char *path, size_t pathlen, + struct ais_t *ais, + /*@null@*/const char **endptr) { + /*@-compdef@*//* splint is confused by storage declared in the .i file */ + /*@-nullstate@*/ #define AIS_HEADER \ {"class", check, .dflt.check = "AIS"}, \ @@ -130,9 +132,11 @@ int json_ais_read(const char *buf, } else if (strstr(buf, "\"type\":24,") != NULL) { status = json_read_object(buf, json_ais24, endptr); } else { - *endptr = NULL; + if (endptr != NULL) + *endptr = NULL; return JSON_ERR_MISC; } + /*@+compdef +nullstate@*/ return status; } diff --git a/gps_json.h b/gps_json.h index 39c99da1..bc65f500 100644 --- a/gps_json.h +++ b/gps_json.h @@ -6,19 +6,20 @@ #define GPS_JSON_RESPONSE_MAX 1024 char *json_stringify(/*@out@*/char *, size_t, /*@in@*/const char *); -void json_tpv_dump(const struct gps_data_t *, struct gps_fix_t *, char *, size_t); -void json_sky_dump(const struct gps_data_t *, char *, size_t); -void json_device_dump(const struct gps_device_t *, char *, size_t); -void json_watch_dump(const struct policy_t *, char *, size_t); +void json_tpv_dump(const struct gps_data_t *, struct gps_fix_t *, + /*@out@*/char *, size_t); +void json_sky_dump(const struct gps_data_t *, /*@out@*/char *, size_t); +void json_device_dump(const struct gps_device_t *, /*@out@*/char *, size_t); +void json_watch_dump(const struct policy_t *, /*@out@*/char *, size_t); int json_watch_read(const char *, /*@out@*/struct policy_t *, - /*@out null@*/const char **); + /*@null@*/const char **); int json_device_read(const char *, /*@out@*/struct devconfig_t *, - /*@out null@*/const char **); + /*@null@*/const char **); void json_version_dump(/*@out@*/char *, size_t); int json_rtcm2_read(const char *, char *, size_t, struct rtcm2_t *, - /*@out null@*/const char **); + /*@null@*/const char **); int json_ais_read(const char *, char *, size_t, struct ais_t *, - /*@out null@*/const char **); + /*@null@*/const char **); int libgps_json_unpack(const char *, struct gps_data_t *); /* gps_json.h ends here */ diff --git a/gpsd.c b/gpsd.c index a7816223..1d1e0203 100644 --- a/gpsd.c +++ b/gpsd.c @@ -1651,6 +1651,14 @@ static void handle_newstyle_request(struct subscriber_t *sub, sub->new_style_responses = true; #endif /* defined(OLDSTYLE_ENABLE) && defined(GPSDNG_ENABLE) */ + /* + * There's a splint limitation that parameters can be declared + * @out@ or @null@ but not, apparently, both. This collides with + * the (admittedly tricky) way we use endptr. The workaround is to + * declare it @null@ and use -compdef around the JSON reader calls. + */ + /*@-compdef@*/ + /* * Still to be implemented: equivalents of Z $ */ @@ -1784,6 +1792,7 @@ static void handle_newstyle_request(struct subscriber_t *sub, } bailout: *after = buf; + /*@+compdef@*/ } #endif /* GPSDNG_ENABLE */ @@ -2380,7 +2389,7 @@ int main(int argc, char *argv[]) */ sub->active = timestamp(); for (channel = channels; channel < channels + NITEMS(channels); channel++) - if (channel->device && channel->subscriber == sub) + if (channel->device!=NULL && channel->subscriber == sub) channel->device->poll_times[sub_index(sub)] = sub->active; if (handle_gpsd_request(sub, buf) < 0) detach_client(sub); @@ -2389,7 +2398,7 @@ int main(int argc, char *argv[]) int devcount = 0, rawcount = 0; /* count devices attached by this subscriber */ for (channel = channels; channel < channels + NITEMS(channels); channel++) - if (channel->device && channel->subscriber == sub) { + if (channel->device!=NULL && channel->subscriber == sub) { devcount++; if (channel->subscriber->policy.raw > 0) rawcount++; diff --git a/gpsd_json.c b/gpsd_json.c index 24b5f6e2..55c77d2b 100644 --- a/gpsd_json.c +++ b/gpsd_json.c @@ -31,7 +31,7 @@ char *json_stringify(/*@out@*/char *to, size_t len, /*@in@*/const char *from) * each character to generate an up to 6-character Java-style * escape */ - for (sp = from; *sp && (tp - to < ((int)len-5)); sp++) { + for (sp = from; *sp!='\0' && ((tp - to) < ((int)len-5)); sp++) { if (iscntrl(*sp)) { *tp++ = '\\'; switch (*sp) { @@ -74,7 +74,7 @@ void json_version_dump(/*@out@*/char *reply, size_t replylen) } void json_tpv_dump(const struct gps_data_t *gpsdata, struct gps_fix_t *fixp, - char *reply, size_t replylen) + /*@out@*/char *reply, size_t replylen) { assert(replylen > 2); (void)strlcpy(reply, "{\"class\":\"TPV\",", replylen); @@ -163,7 +163,8 @@ void json_tpv_dump(const struct gps_data_t *gpsdata, struct gps_fix_t *fixp, (void)strlcat(reply, "}\r\n", sizeof(reply)-strlen(reply)); } -void json_sky_dump(const struct gps_data_t *datap, char *reply, size_t replylen) +void json_sky_dump(const struct gps_data_t *datap, + /*@out@*/char *reply, size_t replylen) { int i, j, used, reported = 0; assert(replylen > 2); @@ -219,48 +220,8 @@ void json_sky_dump(const struct gps_data_t *datap, char *reply, size_t replylen) datap->satellites, reported); } -int json_device_read(const char *buf, - /*@out@*/struct devconfig_t *dev, - /*@out null@*/const char **endptr) -{ - /*@ -fullinitblock @*/ - const struct json_attr_t json_attrs_device[] = { - {"class", check, .dflt.check = "DEVICE"}, - - {"path", string, .addr.string = dev->path, - .len = sizeof(dev->path)}, - {"activated", real, .addr.real = &dev->activated}, - {"flags", integer, .addr.integer = &dev->flags}, - {"driver", string, .addr.string = dev->driver, - .len = sizeof(dev->driver)}, - {"subtype", string, .addr.string = dev->subtype, - .len = sizeof(dev->subtype)}, - {"native", integer, .addr.integer = &dev->driver_mode, - .dflt.integer = -1}, - {"bps", uinteger, .addr.uinteger = &dev->baudrate, - .dflt.uinteger = 0}, - {"parity", character, .addr.character = &dev->parity, - .dflt.character = 'N'}, - {"stopbits", uinteger, .addr.uinteger = &dev->stopbits, - .dflt.uinteger = 1}, - {"cycle", real, .addr.real = &dev->cycle, - .dflt.real = NAN}, - {"mincycle", real, .addr.real = &dev->mincycle, - .dflt.real = NAN}, - {NULL}, - }; - /*@ +fullinitblock @*/ - int status; - - status = json_read_object(buf, json_attrs_device, endptr); - if (status != 0) - return status; - - return 0; -} - void json_device_dump(const struct gps_device_t *device, - char *reply, size_t replylen) + /*@out@*/char *reply, size_t replylen) { char buf1[JSON_VAL_MAX*2+1]; struct classmap_t *cmp; @@ -310,34 +271,8 @@ void json_device_dump(const struct gps_device_t *device, (void)strlcat(reply, "}\r\n", replylen); } -int json_watch_read(const char *buf, - /*@out@*/struct policy_t *ccp, - /*@out null@*/const char **endptr) -{ - int intcasoc; - /*@ -fullinitblock @*/ - struct json_attr_t chanconfig_attrs[] = { - {"enable", boolean, .addr.boolean = &ccp->watcher, - .dflt.boolean = true}, - {"raw", integer, .addr.integer = &ccp->raw, - .nodefault = true}, - {"buffer_policy", integer, .addr.integer = &intcasoc, - .dflt.integer = -1}, - {"scaled", boolean, .addr.boolean = &ccp->scaled}, - {NULL}, - }; - /*@ +fullinitblock @*/ - int status; - - status = json_read_object(buf, chanconfig_attrs, endptr); - if (status == 0) { - if (intcasoc != -1) - ccp->buffer_policy = intcasoc; - } - return status; -} - -void json_watch_dump(const struct policy_t *ccp, char *reply, size_t replylen) +void json_watch_dump(const struct policy_t *ccp, + /*@out@*/char *reply, size_t replylen) { (void)snprintf(reply+strlen(reply), replylen-strlen(reply), "{\"class\":\"WATCH\",\"enable\":%s,\"raw\":%d,\"buffer_policy\":%d,\"scaled\":%s}\r\n", @@ -351,6 +286,7 @@ void json_watch_dump(const struct policy_t *ccp, char *reply, size_t replylen) void rtcm2_json_dump(const struct rtcm2_t *rtcm, /*@out@*/char buf[], size_t buflen) /* dump the contents of a parsed RTCM104 message as JSON */ { + /*@-mustfreefresh@*/ char buf1[JSON_VAL_MAX*2+1]; /* * Beware! Needs to stay synchronized with a JSON enumeration map in @@ -474,6 +410,7 @@ void rtcm2_json_dump(const struct rtcm2_t *rtcm, /*@out@*/char buf[], size_t buf if (buf[strlen(buf)-1] == ',') buf[strlen(buf)-1] = '\0'; (void)strlcat(buf, "}\r\n", buflen); + /*@+mustfreefresh@*/ } #endif /* defined(RTCM104V2_ENABLE) */ @@ -663,7 +600,7 @@ void aivdm_json_dump(const struct ais_t *ais, bool scaled, /*@out@*/char *buf, s ais->type, ais->repeat, ais->mmsi); #define JSON_BOOL(x) ((x)?"true":"false") - /*@ -formatcode @*/ + /*@ -formatcode -mustfreefresh @*/ switch (ais->type) { case 1: /* Position Report */ case 2: @@ -1221,10 +1158,77 @@ void aivdm_json_dump(const struct ais_t *ais, bool scaled, /*@out@*/char *buf, s (void) strlcat(buf, "}\r\n", buflen); break; } - /*@ +formatcode @*/ + /*@ +formatcode +mustfreefresh @*/ #undef SHOW_BOOL } #endif /* defined(AIVDM_ENABLE) */ +int json_device_read(const char *buf, + /*@out@*/struct devconfig_t *dev, + /*@null@*/const char **endptr) +{ + /*@ -fullinitblock @*/ + const struct json_attr_t json_attrs_device[] = { + {"class", check, .dflt.check = "DEVICE"}, + + {"path", string, .addr.string = dev->path, + .len = sizeof(dev->path)}, + {"activated", real, .addr.real = &dev->activated}, + {"flags", integer, .addr.integer = &dev->flags}, + {"driver", string, .addr.string = dev->driver, + .len = sizeof(dev->driver)}, + {"subtype", string, .addr.string = dev->subtype, + .len = sizeof(dev->subtype)}, + {"native", integer, .addr.integer = &dev->driver_mode, + .dflt.integer = -1}, + {"bps", uinteger, .addr.uinteger = &dev->baudrate, + .dflt.uinteger = 0}, + {"parity", character, .addr.character = &dev->parity, + .dflt.character = 'N'}, + {"stopbits", uinteger, .addr.uinteger = &dev->stopbits, + .dflt.uinteger = 1}, + {"cycle", real, .addr.real = &dev->cycle, + .dflt.real = NAN}, + {"mincycle", real, .addr.real = &dev->mincycle, + .dflt.real = NAN}, + {NULL}, + }; + /*@ +fullinitblock @*/ + int status; + + status = json_read_object(buf, json_attrs_device, endptr); + if (status != 0) + return status; + + return 0; +} + +int json_watch_read(const char *buf, + /*@out@*/struct policy_t *ccp, + /*@null@*/const char **endptr) +{ + int intcasoc = -1; + /*@ -fullinitblock @*/ + struct json_attr_t chanconfig_attrs[] = { + {"enable", boolean, .addr.boolean = &ccp->watcher, + .dflt.boolean = true}, + {"raw", integer, .addr.integer = &ccp->raw, + .nodefault = true}, + {"buffer_policy", integer, .addr.integer = &intcasoc, + .dflt.integer = -1}, + {"scaled", boolean, .addr.boolean = &ccp->scaled}, + {NULL}, + }; + /*@ +fullinitblock @*/ + int status; + + status = json_read_object(buf, chanconfig_attrs, endptr); + if (status == 0) { + if (intcasoc != -1) + ccp->buffer_policy = intcasoc; + } + return status; +} + /* gpsd_json.c ends here */ diff --git a/json.c b/json.c index 245c77d1..cb886a3f 100644 --- a/json.c +++ b/json.c @@ -95,8 +95,9 @@ static int json_internal_read_object(const char *cp, const struct json_attr_t *attrs, const struct json_array_t *parent, int offset, - /*@out null@*/const char **end) + /*@null@*/const char **end) { + /*@ -nullstate -nullderef -mustfreefresh @*/ enum {init, await_attr, in_attr, await_value, in_val_string, in_escape, in_val_token, post_val} state = 0; #ifdef JSONDEBUG @@ -111,6 +112,7 @@ static int json_internal_read_object(const char *cp, char uescape[5]; /* enough space for 4 hex digits and a NUL */ const struct json_attr_t *cursor; int substatus, maxlen, n; + unsigned int u; const struct json_enum_t *mp; char *lptr; @@ -121,6 +123,7 @@ 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: @@ -139,8 +142,10 @@ static int json_internal_read_object(const char *cp, break; case boolean: /* nullbool default says not to set the value at all */ + /*@+boolint@*/ if (cursor->dflt.boolean != nullbool) *((bool *)lptr) = cursor->dflt.boolean; + /*@-boolint@*/ break; case character: lptr[0] = cursor->dflt.character; @@ -151,12 +156,13 @@ static int json_internal_read_object(const char *cp, case check: break; } + /*@+nullderef@*/ } json_debug_trace(("JSON parse begins.\n")); /* parse input JSON */ - for (; *cp; cp++) { + for (; *cp!='\0'; cp++) { json_debug_trace(("State %-14s, looking at '%c' (%p)\n", statenames[state], *cp, cp)); switch (state) { @@ -198,9 +204,9 @@ static int json_internal_read_object(const char *cp, if (cursor->type == string) maxlen = (int)cursor->len - 1; else if (cursor->type == check) - maxlen = strlen(cursor->dflt.check); + maxlen = (int)strlen(cursor->dflt.check); else if (cursor->map != NULL) - maxlen = sizeof(valbuf)-1; + maxlen = (int)sizeof(valbuf)-1; pval = valbuf; } else if (pattr >= attrbuf + JSON_ATTR_MAX - 1) { json_debug_trace(("Attribute name too long.\n")); @@ -268,8 +274,8 @@ static int json_internal_read_object(const char *cp, for (n = 0; n < 4 && cp[n] != '\0'; n++) uescape[n] = *cp++; --cp; - (void)sscanf(uescape, "%04x", &n); - *pval++ = (char)n; /* will truncate values above 0xff */ + (void)sscanf(uescape, "%04x", &u); + *pval++ = (char)u; /* will truncate values above 0xff */ break; default: /* handles double quote and solidus */ *pval++ = *cp; @@ -310,6 +316,7 @@ 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: @@ -346,6 +353,7 @@ static int json_internal_read_object(const char *cp, } break; } + /*@+nullderef@*/ if (isspace(*cp)) continue; else if (*cp == ',') @@ -366,6 +374,7 @@ good_parse: *end = cp; json_debug_trace(("JSON parse ends.\n")); return 0; + /*@ +nullstate +nullderef +mustfreefresh @*/ } int json_read_array(const char *cp, const struct json_array_t *arr, const char **end) @@ -457,7 +466,7 @@ breakout: int json_read_object(const char *cp, const struct json_attr_t *attrs, - /*@out null@*/const char **end) + /*@null@*/const char **end) { return json_internal_read_object(cp, attrs, NULL, 0, end); } diff --git a/json.h b/json.h index 28e33afc..98947924 100644 --- a/json.h +++ b/json.h @@ -61,9 +61,9 @@ struct json_attr_t { #define JSON_VAL_MAX 120 /* max chars in JSON value part */ int json_read_object(const char *, const struct json_attr_t *, - /*@out null@*/const char **); + /*@null@*/const char **); int json_read_array(const char *, const struct json_array_t *, - /*@out null@*/const char **); + /*@null@*/const char **); const /*@observer@*/char *json_error_string(int); #define JSON_ERR_OBSTART 1 /* non-WS when expecting object start */ diff --git a/libgps.c b/libgps.c index 8ec4d4cc..a71fe0b4 100644 --- a/libgps.c +++ b/libgps.c @@ -225,7 +225,7 @@ int gps_unpack(char *buf, struct gps_data_t *gpsdata) if (sp[2] == '?') gpsdata->dev.driver_mode = MODE_NMEA; else - gpsdata->dev.driver_mode = (unsigned)atoi(sp+2); + gpsdata->dev.driver_mode = atoi(sp+2); break; case 'O': if (sp[2] == '?') { diff --git a/libgps_json.c b/libgps_json.c index 23928398..2edb46b3 100644 --- a/libgps_json.c +++ b/libgps_json.c @@ -19,9 +19,17 @@ representations to libgps structures. #include "gpsd.h" #include "gps_json.h" +/* + * There's a splint limitation that parameters can be declared + * @out@ or @null@ but not, apparently, both. This collides with + * the (admittedly tricky) way we use endptr. The workaround is to + * declare it @null@ and use -compdef around the JSON reader calls. + */ +/*@-compdef@*/ + static int json_tpv_read(const char *buf, struct gps_data_t *gpsdata, - /*@out null@*/const char **endptr) + /*@null@*/const char **endptr) { int status; /*@ -fullinitblock @*/ @@ -104,7 +112,7 @@ static int json_tpv_read(const char *buf, static int json_sky_read(const char *buf, struct gps_data_t *gpsdata, - /*@out null@*/const char **endptr) + /*@null@*/const char **endptr) { bool usedflags[MAXCHANNELS]; /*@ -fullinitblock @*/ @@ -152,7 +160,7 @@ static int json_sky_read(const char *buf, static int json_devicelist_read(const char *buf, struct gps_data_t *gpsdata, - /*@out null@*/const char **endptr) + /*@null@*/const char **endptr) { /*@ -fullinitblock @*/ const struct json_attr_t json_attrs_subdevices[] = { @@ -179,6 +187,7 @@ static int json_devicelist_read(const char *buf, .dflt.real = NAN}, {NULL}, }; + /*@-type@*//* STRUCTARRAY confuses splint */ const struct json_attr_t json_attrs_devices[] = { {"class", check, .dflt.check = "DEVICES"}, {"devices", array, STRUCTARRAY(gpsdata->devices.list, @@ -186,6 +195,7 @@ static int json_devicelist_read(const char *buf, &gpsdata->devices.ndevices)}, {NULL}, }; + /*@+type@*/ /*@ +fullinitblock @*/ int status; @@ -201,7 +211,7 @@ static int json_devicelist_read(const char *buf, static int json_version_read(const char *buf, struct gps_data_t *gpsdata, - /*@out null@*/const char **endptr) + /*@null@*/const char **endptr) { /*@ -fullinitblock @*/ const struct json_attr_t json_attrs_version[] = { @@ -228,7 +238,7 @@ static int json_version_read(const char *buf, static int json_error_read(const char *buf, struct gps_data_t *gpsdata, - /*@out null@*/const char **endptr) + /*@null@*/const char **endptr) { /*@ -fullinitblock @*/ const struct json_attr_t json_attrs_error[] = { @@ -294,5 +304,6 @@ int libgps_json_unpack(const char *buf, struct gps_data_t *gpsdata) } else return -1; } +/*@+compdef@*/ /* libgps_json.c ends here */ diff --git a/libgpsd_core.c b/libgpsd_core.c index 25797a6f..44d42103 100644 --- a/libgpsd_core.c +++ b/libgpsd_core.c @@ -717,7 +717,7 @@ gps_mask_t gpsd_poll(struct gps_device_t *session) session->gpsdata.dev.path, session->packet.type); if (session->packet.type > COMMENT_PACKET) { - session->observed |= PACKET_TYPEMASK(session->packet.type); + /*@i1@*/session->observed |= PACKET_TYPEMASK(session->packet.type); first_sync = (session->device_type == NULL); for (dp = gpsd_drivers; *dp; dp++) if (session->packet.type == (*dp)->packet_type) { diff --git a/rtcm2_json.c b/rtcm2_json.c index 67ba5dc9..fac27f29 100644 --- a/rtcm2_json.c +++ b/rtcm2_json.c @@ -24,7 +24,7 @@ representations to libgps structures. int json_rtcm2_read(const char *buf, char *path, size_t pathlen, struct rtcm2_t *rtcm2, - const char **endptr) + /*@null@*/const char **endptr) { static char *stringptrs[NITEMS(rtcm2->words)]; @@ -54,12 +54,14 @@ int json_rtcm2_read(const char *buf, {"rangerate", real, STRUCTOBJECT(struct rangesat_t, rangerate)}, {NULL}, }; + /*@-type@*//* STRUCTARRAY confuses splint */ const struct json_attr_t json_rtcm1[] = { RTCM2_HEADER {"satellites", array, STRUCTARRAY(rtcm2->ranges.sat, rtcm1_satellite, &satcount)}, {NULL}, }; + /*@+type@*/ const struct json_attr_t json_rtcm3[] = { RTCM2_HEADER @@ -109,12 +111,14 @@ int json_rtcm2_read(const char *buf, {"tou", uinteger, STRUCTOBJECT(struct consat_t, tou)}, {NULL}, }; + /*@-type@*//* STRUCTARRAY confuses splint */ const struct json_attr_t json_rtcm5[] = { RTCM2_HEADER {"satellites", array, STRUCTARRAY(rtcm2->conhealth.sat, rtcm5_satellite, &satcount)}, {NULL}, }; + /*@+type@*/ const struct json_attr_t json_rtcm6[] = { RTCM2_HEADER @@ -132,12 +136,14 @@ int json_rtcm2_read(const char *buf, {"bitrate", uinteger, STRUCTOBJECT(struct station_t, bitrate)}, {NULL}, }; + /*@-type@*//* STRUCTARRAY confuses splint */ const struct json_attr_t json_rtcm7[] = { RTCM2_HEADER {"satellites", array, STRUCTARRAY(rtcm2->almanac.station, rtcm7_satellite, &satcount)}, {NULL}, }; + /*@+type@*/ const struct json_attr_t json_rtcm16[] = { RTCM2_HEADER @@ -146,6 +152,7 @@ int json_rtcm2_read(const char *buf, {NULL}, }; + /*@-type@*//* complex union array initislizations confuses splint */ const struct json_attr_t json_rtcm2_fallback[] = { RTCM2_HEADER {"data", array, .addr.array.element_type = string, @@ -156,6 +163,7 @@ int json_rtcm2_read(const char *buf, .addr.array.maxlen = NITEMS(stringptrs)}, {NULL}, }; + /*@+type@*/ /*@ +fullinitblock @*/ #undef RTCM2_HEADER -- cgit v1.2.1