summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--gpsctl.c6
-rw-r--r--gpsd.c3
-rw-r--r--gpsd.h-tail5
-rw-r--r--gpsdecode.c7
-rw-r--r--gpsmon.c9
-rw-r--r--libgps_core.c2
-rw-r--r--libgpsd_core.c14
-rw-r--r--test_packet.c8
8 files changed, 29 insertions, 25 deletions
diff --git a/gpsctl.c b/gpsctl.c
index c4029d3e..6ea4a123 100644
--- a/gpsctl.c
+++ b/gpsctl.c
@@ -304,8 +304,6 @@ int main(int argc, char **argv)
}
}
- context.errout.label = "gpsctl";
-
if (optind < argc)
device = argv[optind];
@@ -568,7 +566,7 @@ int main(int argc, char **argv)
}
/*@ -mustfreeonly -immediatetrans @*/
- gps_context_init(&context);
+ gps_context_init(&context, "gpsctl");
context.errout.debug = debuglevel;
session.context = &context;
gpsd_tty_init(&session);
@@ -604,7 +602,7 @@ int main(int argc, char **argv)
*/
/*@ -mustfreeonly -immediatetrans @*/
- gps_context_init(&context);
+ gps_context_init(&context, "gpsctl");
context.errout.debug = debuglevel;
session.context = &context; /* in case gps_init isn't called */
diff --git a/gpsd.c b/gpsd.c
index 09690620..ed3ba1f0 100644
--- a/gpsd.c
+++ b/gpsd.c
@@ -1812,8 +1812,7 @@ int main(int argc, char *argv[])
bool go_background = true;
volatile bool in_restart;
- gps_context_init(&context);
- context.errout.label = "gpsd";
+ gps_context_init(&context, "gpsd");
#ifdef CONTROL_SOCKET_ENABLE
INVALIDATE_SOCKET(csock);
diff --git a/gpsd.h-tail b/gpsd.h-tail
index 7f0ebc39..7b62ce1e 100644
--- a/gpsd.h-tail
+++ b/gpsd.h-tail
@@ -944,7 +944,8 @@ extern int srec_fin(unsigned int, unsigned char *);
extern unsigned char hc(unsigned char);
/* application interface */
-extern void gps_context_init(struct gps_context_t *context);
+extern void gps_context_init(struct gps_context_t *context,
+ /*@observer@*/const char *label);
extern void gpsd_init(struct gps_device_t *,
struct gps_context_t *,
/*@null@*/const char *);
@@ -1005,7 +1006,7 @@ void gpsd_labeled_report(const int, const int,
# if __GNUC__ >= 3 || (__GNUC__ == 2 && __GNUC_MINOR__ >= 7)
__attribute__((__format__(__printf__, 3, 4))) void gpsd_report(const struct gpsd_errout_t *, const int, const char *, ...);
# else /* not a new enough GCC, use the unprotected prototype */
-void gpsd_report(const struct *gpsd_errout_t, const int, const char *, ...);
+void gpsd_report(const struct gpsd_errout_t *, const int, const char *, ...);
#endif
#ifdef S_SPLINT_S
diff --git a/gpsdecode.c b/gpsdecode.c
index 68e4c68b..abf154c2 100644
--- a/gpsdecode.c
+++ b/gpsdecode.c
@@ -508,7 +508,7 @@ static bool filter(gps_mask_t changed, struct gps_device_t *session)
return false;
}
-/*@ -compdestroy -compdef -usedef -uniondef @*/
+/*@ -mustfreeonly -compdestroy -compdef -usedef -uniondef -immediatetrans -observertrans -statictrans @*/
static void decode(FILE *fpin, FILE*fpout)
/* sensor data on fpin to dump format on fpout */
{
@@ -523,10 +523,9 @@ static void decode(FILE *fpin, FILE*fpout)
policy.json = json;
policy.scaled = scaled;
- gps_context_init(&context);
+ gps_context_init(&context, "gpsdecode");
gpsd_time_init(&context, time(NULL));
context.readonly = true;
- context.errout.label = "gpsdecode";
gpsd_init(&session, &context, NULL);
gpsd_clear(&session);
session.gpsdata.gps_fd = fileno(fpin);
@@ -623,7 +622,7 @@ static void encode(FILE *fpin, FILE *fpout)
(void)fputs(inbuf, fpout);
}
}
-/*@ +compdestroy +compdef +usedef @*/
+/*@ +mustfreeonly +compdestroy +compdef +usedef +immediatetrans +observertrans @ +statictrans*/
#endif /* SOCKET_EXPORT_ENABLE */
int main(int argc, char **argv)
diff --git a/gpsmon.c b/gpsmon.c
index c60b9870..c812063b 100644
--- a/gpsmon.c
+++ b/gpsmon.c
@@ -250,7 +250,7 @@ static void monitor_dump_send(/*@in@*/ const char *buf, size_t len)
#endif /* defined(CONTROLSEND_ENABLE) || defined(RECONFIGURE_ENABLE) */
/*@-compdef@*/
-static void report_hook(const char *buf)
+static void gpsmon_report(const char *buf)
{
char buf2[BUFSIZ];
@@ -271,7 +271,7 @@ static void report_hook(const char *buf)
static void packet_vlog(/*@out@*/char *buf, size_t len, const char *fmt, va_list ap)
{
(void)vsnprintf(buf + strlen(buf), len, fmt, ap);
- report_hook(buf);
+ gpsmon_report(buf);
}
/*@+compdef@*/
@@ -1054,10 +1054,9 @@ int main(int argc, char **argv)
/*@ -observertrans @*/
(void)putenv("TZ=UTC"); // for ctime()
/*@ +observertrans @*/
- gps_context_init(&context); // initialize the report mutex
+ gps_context_init(&context, "gsmon"); // initialize the report mutex
context.serial_write = gpsmon_serial_write;
- context.errout.label = "gpsmon";
- context.errout.report = report_hook;
+ context.errout.report = gpsmon_report;
while ((option = getopt(argc, argv, "aD:LVhl:nt:?")) != -1) {
switch (option) {
case 'a':
diff --git a/libgps_core.c b/libgps_core.c
index a222ae13..42c5051c 100644
--- a/libgps_core.c
+++ b/libgps_core.c
@@ -145,8 +145,10 @@ int gps_read(struct gps_data_t *gpsdata)
#endif /* SOCKET_EXPORT_ENABLE */
/*@ +usedef +compdef +uniondef @*/
+ /*@-usedef@*/
libgps_debug_trace((DEBUG_CALLS, "gps_read() -> %d (%s)\n",
status, gps_maskdump(gpsdata->set)));
+ /*@+usedef@*/
return status;
}
diff --git a/libgpsd_core.c b/libgpsd_core.c
index 7b8c6774..6cade557 100644
--- a/libgpsd_core.c
+++ b/libgpsd_core.c
@@ -245,11 +245,12 @@ int gpsd_switch_driver(struct gps_device_t *session, char *type_name)
}
/*@+kepttrans@*/
-/*@-compdestroy@*/
-void gps_context_init(struct gps_context_t *context)
+/*@-compdestroy -mustfreeonly -observertrans -dependenttrans@*/
+void gps_context_init(struct gps_context_t *context,
+ /*@observer@*/const char *label)
{
/* *INDENT-OFF* */
- /*@ -initallelements -nullassign -nullderef @*/
+ /*@ -initallelements -nullassign -nullderef -fullinitblock @*/
struct gps_context_t nullcontext = {
.valid = 0,
.readonly = false,
@@ -275,11 +276,12 @@ void gps_context_init(struct gps_context_t *context)
#endif /* SHM_EXPORT_ENABLE */
.serial_write = gpsd_serial_write,
};
- /*@ +initallelements +nullassign +nullderef @*/
+ /*@ +initallelements +nullassign +nullderef +fullinitblock @*/
/* *INDENT-ON* */
(void)memcpy(context, &nullcontext, sizeof(struct gps_context_t));
errout_reset(&context->errout);
+ context->errout.label = label;
#if !defined(S_SPLINT_S) && defined(PPS_ENABLE)
/*@-nullpass@*/
@@ -287,7 +289,7 @@ void gps_context_init(struct gps_context_t *context)
/*@+nullpass@*/
#endif /* defined(S_SPLINT_S) defined(PPS_ENABLE) */
}
-/*@+compdestroy@*/
+/*@+compdestroy +mustfreeonly +observertrans +dependenttrans@*/
void gpsd_init(struct gps_device_t *session, struct gps_context_t *context,
const char *device)
@@ -364,6 +366,7 @@ void gpsd_deactivate(struct gps_device_t *session)
session->gpsdata.online = (timestamp_t)0;
}
+/*@-usereleased -compdef@*/
void gpsd_clear(struct gps_device_t *session)
{
session->gpsdata.online = timestamp();
@@ -385,6 +388,7 @@ void gpsd_clear(struct gps_device_t *session)
session->opentime = timestamp();
}
+/*@+usereleased +compdef@*/
int gpsd_open(struct gps_device_t *session)
/* open a device for access to its data */
diff --git a/test_packet.c b/test_packet.c
index da52c033..88cfec51 100644
--- a/test_packet.c
+++ b/test_packet.c
@@ -255,6 +255,7 @@ static struct map runontests[] = {
static int packet_test(struct map *mp)
{
+ /*@-compdestroy@*/
struct gps_lexer_t lexer;
int failure = 0;
@@ -278,8 +279,10 @@ static int packet_test(struct map *mp)
mp->legend); /*@ +compdef +uniondef +usedef +formatcode @*/
return failure;
+ /*@+compdestroy@*/
}
+/*@ -compdef -uniondef -usedef -formatcode -compdestroy @*/
static void runon_test(struct map *mp)
{
struct gps_lexer_t lexer;
@@ -290,14 +293,13 @@ static void runon_test(struct map *mp)
lexer.errout.debug = verbose;
/*@i@*/ memcpy(lexer.inbufptr = lexer.inbuffer, mp->test, mp->testlen);
lexer.inbuflen = mp->testlen;
- /*@ -compdef -uniondef -usedef -formatcode @*/
- (void)fputs(mp->test, stdout);
+ (void)fputs(mp->test, stdout);
do {
st = packet_get(nullfd, &lexer);
//printf("packet_parse() returned %zd\n", st);
} while (st > 0);
- /*@ +compdef +uniondef +usedef +formatcode @*/
}
+/*@ +compdef +uniondef +usedef +formatcode +compdestroy@*/
static int property_check(void)
{
View Lorry Controller Status