メインコンテンツ

ISO/IEC TS 17961 [ioileave]

Interleaving stream inputs and outputs without a flush or positioning call

説明

ルール定義

フラッシュまたは位置付け呼び出しなしでのストリーム入出力のインターリーブ。1

Polyspace 実装

このチェッカーは、フラッシュまたは位置付け呼び出しなしでのストリームからの入出力の交互実行をチェックします。

すべて展開する

問題

フラッシュまたは位置付け呼び出しなしでのストリームからの入出力の交互実行は次の場合に発生します。

  • 更新モードのファイル ストリームにおける出力操作とそれに続く入力操作の間でフラッシュまたは関数位置付け呼び出しを実行しない。

  • 更新モードのファイル ストリームにおける入力操作とそれに続く出力操作の間で関数位置付け呼び出しを実行しない。

リスク

介在するフラッシュまたは位置付け呼び出しなしでのストリームにおける入出力操作の交互実行は未定義の動作です。

修正方法

更新ストリームにおける入出力操作間で fflush() または fseek()fsetpos() などのファイル位置付け関数を呼び出します。

更新ストリームにおける入出力操作間でファイル位置付け関数を呼び出します。

例 - 介在するフラッシュなしでの読み取り後の書き込み
#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. */;
      }
}
        
      

この例では、ファイル demo.txt は読み取りおよび追加のために開かれています。fwrite() の呼び出し後に行われる、介在するフラッシュ操作なしでの fread() の呼び出しは未定義の動作です。

修正 — 読み取り操作の前に fflush() を呼び出す

データをファイルに書き込んだ後、fread() を呼び出す前にフラッシュ呼び出しを実行します。

#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. */;
      }
} 

チェック情報

決定可能性:決定不可能

バージョン履歴

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.