diff --git a/src/include/pv-internal.h b/src/include/pv-internal.h
index d7f96de..101505f 100644
--- a/src/include/pv-internal.h
+++ b/src/include/pv-internal.h
@@ -131,6 +131,7 @@ typedef uint16_t pvdisplay_bytecount_t;
 typedef uint16_t pvdisplay_width_t;
 #define PVDISPLAY_WIDTH_MAX (65535)	/* UINT16_MAX */
 
+typedef /*@only@*/ /*@null@*/ char * nullable_string_t;
 
 /*
  * Structure for holding PV internal state. Opaque outside the PV library.
@@ -154,7 +155,7 @@ struct pvstate_s {
 	 * Input files *
 	 ***************/
 	struct pvinputfiles_s {
-		/*@only@*/ /*@null@*/ char **filename; /* input filenames */
+		/*@only@*/ /*@null@*/ nullable_string_t *filename; /* input filenames */
 		unsigned int file_count;	 /* number of input files */
 	} files;
 
diff --git a/src/pv/file.c b/src/pv/file.c
index d71c903..512f001 100644
--- a/src/pv/file.c
+++ b/src/pv/file.c
@@ -54,6 +54,10 @@ static off_t pv_calc_total_bytes(pvstate_t state)
 	for (file_idx = 0; file_idx < state->files.file_count; file_idx++) {
 		int rc;
 
+		/* Skip any NULL entries, though they should be impossible. */
+		if (NULL == state->files.filename[file_idx])
+			continue;
+
 		if (0 == strcmp(state->files.filename[file_idx], "-")) {
 			rc = fstat(STDIN_FILENO, &sb);
 			if (rc != 0) {
@@ -187,6 +191,10 @@ static off_t pv_calc_total_lines(pvstate_t state)
 		int fd = -1;
 		int rc = 0;
 
+		/* Skip any NULL entries, though they should be impossible. */
+		if (NULL == state->files.filename[file_idx])
+			continue;
+
 		if (0 == strcmp(state->files.filename[file_idx], "-")) {
 			rc = fstat(STDIN_FILENO, &sb);
 			if ((rc != 0) || (!S_ISREG(sb.st_mode))) {
@@ -288,6 +296,7 @@ int pv_next_file(pvstate_t state, unsigned int filenum, int oldfd)
 	struct stat osb;
 	int fd;
 	bool input_file_is_output;
+	char *next_filename;
 
 	if (oldfd >= 0) {
 		if (0 != close(oldfd)) {
@@ -303,10 +312,20 @@ int pv_next_file(pvstate_t state, unsigned int filenum, int oldfd)
 		return -1;
 	}
 
-	if ((NULL == state->files.filename) || (0 == strcmp(state->files.filename[filenum], "-"))) {
+	next_filename = NULL;
+	if (NULL != state->files.filename) {
+		next_filename = state->files.filename[filenum];
+		if (NULL == next_filename) {
+			debug("%s: @%d, max %d", "unexpected null filename", filenum, state->files.file_count);
+			state->status.exit_status |= PV_ERROREXIT_TRANSITION;
+			return -1;
+		}
+	}
+
+	if ((NULL == next_filename) || (0 == strcmp(next_filename, "-"))) {
 		fd = STDIN_FILENO;
 	} else {
-		fd = open(state->files.filename[filenum], O_RDONLY);	/* flawfinder: ignore */
+		fd = open(next_filename, O_RDONLY);		/* flawfinder: ignore */
 		/*
 		 * flawfinder rationale: the input file list is under the
 		 * control of the operator by its nature, so we can't refuse
@@ -314,7 +333,7 @@ int pv_next_file(pvstate_t state, unsigned int filenum, int oldfd)
 		 */
 		if (fd < 0) {
 			pv_error("%s: %s: %s",
-				 _("failed to read file"), state->files.filename[filenum], strerror(errno));
+				 _("failed to read file"), next_filename, strerror(errno));
 			state->status.exit_status |= PV_ERROREXIT_ACCESS;
 			return -1;
 		}
@@ -322,7 +341,7 @@ int pv_next_file(pvstate_t state, unsigned int filenum, int oldfd)
 
 	if (0 != fstat(fd, &isb)) {
 		pv_error("%s: %s: %s", _("failed to stat file"),
-			 NULL == state->files.filename ? "-" : state->files.filename[filenum], strerror(errno));
+			 NULL == next_filename ? "-" : next_filename, strerror(errno));
 		(void) close(fd);
 		state->status.exit_status |= PV_ERROREXIT_ACCESS;
 		return -1;
@@ -352,7 +371,7 @@ int pv_next_file(pvstate_t state, unsigned int filenum, int oldfd)
 
 	if (input_file_is_output) {
 		pv_error("%s: %s", _("input file is output file"),
-			 NULL == state->files.filename ? "-" : state->files.filename[filenum]);
+			 NULL == next_filename ? "-" : next_filename);
 		(void) close(fd);
 		state->status.exit_status |= PV_ERROREXIT_OUROBOROS;
 		return -1;
diff --git a/src/pv/state.c b/src/pv/state.c
index 1b0b84e..a7d0061 100644
--- a/src/pv/state.c
+++ b/src/pv/state.c
@@ -667,41 +667,39 @@ void pv_state_set_terminal_supports_utf8(pvstate_t state, bool val)
 void pv_state_inputfiles(pvstate_t state, unsigned int input_file_count, const char **input_files)
 {
 	unsigned int file_idx;
+	/*@only@*/ nullable_string_t *new_array;
 
+	/* Free the old array and its contents, if there was one. */
 	if (NULL != state->files.filename) {
 		for (file_idx = 0; file_idx < state->files.file_count; file_idx++) {
-			/*@-unqualifiedtrans@ */
 			free(state->files.filename[file_idx]);
-			/*@+unqualifiedtrans@ */
-			/*
-			 * TODO: find a way to tell splint the array
-			 * contents are "only" and "null" as well as the
-			 * array itself.
-			 */
 		}
 		free(state->files.filename);
 		state->files.filename = NULL;
 		state->files.file_count = 0;
 	}
-	state->files.filename = calloc((size_t) (input_file_count + 1), sizeof(char *));
-	if (NULL == state->files.filename) {
+
+	/* Allocate an empty new array of the right size. */
+	new_array = calloc((size_t) (input_file_count + 1), sizeof(char *));
+	if (NULL == new_array) {
 		/*@-mustfreefresh@ *//* see similar _() issue above */
 		pv_error("%s: %s", _("file list allocation failed"), strerror(errno));
 		/*@+mustfreefresh@ */
 		return;
 	}
+	state->files.filename = new_array;
+
+	/* Populate the new array with copies of the filenames. */
 	for (file_idx = 0; file_idx < input_file_count; file_idx++) {
-		/*@-nullstate@ */
-		state->files.filename[file_idx] = pv_strdup(input_files[file_idx]);
-		if (NULL == state->files.filename[file_idx]) {
+		/*@only@*/ char *new_string;
+		new_string = pv_strdup(input_files[file_idx]);
+		if (NULL == new_string) {
 			/*@-mustfreefresh@ *//* see similar _() issue above */
 			pv_error("%s: %s", _("file list allocation failed"), strerror(errno));
 			/*@+mustfreefresh@ */
 			return;
 		}
+		state->files.filename[file_idx] = new_string;
 	}
 	state->files.file_count = input_file_count;
 }
-
-/*@+nullstate@*/
-/* splint: see unqualifiedtrans note by free() above. */