Main Content

ISO/IEC TS 17961 [ioileave]

Interleaving stream inputs and outputs without a flush or positioning call

Description

Rule Definition

Interleaving stream inputs and outputs without a flush or positioning call.1

Polyspace Implementation

This checker checks for Alternating input and output from a stream without flush or positioning call.

Examples

expand all

Issue

Alternating input and output from a stream without flush or positioning call occurs when:

  • You do not perform a flush or function positioning call between an output operation and a following input operation on a file stream in update mode.

  • You do not perform a function positioning call between an input operation and a following output operation on a file stream in update mode.

Risk

Alternating input and output operations on a stream without an intervening flush or positioning call is undefined behavior.

Fix

Call fflush() or a file positioning function such as fseek() or fsetpos() between output and input operations on an update stream.

Call a file positioning function between input and output operations on an update stream.

Example - Read After Write Without Intervening Flush
#include <stdio.h>
#define SIZE20 20

void initialize_data(char* data, size_t s) {};
const char *temp_filename = "/tmp/demo.txt";

void func()
{
    char data[SIZE20];
    char append_data[SIZE20];
    FILE *file;

    file = fopen(temp_filename, "a+");
    if (file == NULL)
      {
        /* Handle error. */;
      }

    initialize_data(append_data, SIZE20);

    if (fwrite(append_data, 1, SIZE20, file) != SIZE20)
      {
        (void)fclose(file);
        /* Handle error. */;
      }
	/* Read operation after write without 
	intervening flush. */
    if (fread(data, 1, SIZE20, file) < SIZE20)  
      {
          (void)fclose(file);
          /* Handle error. */;
      }

    if (fclose(file) == EOF)
      {
        /* Handle error. */;
      }
}
        
      

In this example, the file demo.txt is opened for reading and appending. After the call to fwrite(), a call to fread() without an intervening flush operation is undefined behavior.

Correction — Call fflush() Before the Read Operation

After writing data to the file, before calling fread(), perform a flush call.

#include <stdio.h>
#define SIZE20 20

void initialize_data(char* data, size_t s) {};
const char *temp_filename = "/tmp/demo.txt";


void func()
{
    char data[SIZE20];
    char append_data[SIZE20];
    FILE *file;

    file = fopen(temp_filename, "a+");
    if (file == NULL)
      {
        /* Handle error. */;
      }

    initialize_data(append_data, SIZE20);

    if (fwrite(append_data, 1, SIZE20, file) != SIZE20)
      {
        (void)fclose(file);
        /* Handle error. */;
      }
	/* Buffer flush after write and before read */
    if (fflush(file) != 0)  
      {
        (void)fclose(file);
        /* Handle error. */;
      }
    if (fread(data, 1, SIZE20, file) < SIZE20)
      {
        (void)fclose(file);
        /* Handle error. */;
      }

    if (fclose(file) == EOF)
      {
        /* Handle error. */;
      }
} 

Check Information

Decidability: Undecidable

Version History

Introduced in R2019a


1 Extracts from the standard "ISO/IEC TS 17961 Technical Specification - 2013-11-15" are reproduced with the agreement of AFNOR. Only the original and complete text of the standard, as published by AFNOR Editions - accessible via the website www.boutique.afnor.org - has normative value.