memset と memcpy に関する Code Prover の仮定
ライブラリ関数 memset および memcpy と、これらのライブラリ関数にオプション -code-behavior-specifications を使用してマッピングされた関数には、以下の仮定が適用されます。
memcpy 向けの Polyspace 仕様
構文:
#include <string.h> void * memcpy ( void * destinationPtr, const void * sourcePtr, size_t num );
コードが関数 memcpy を使用する場合、この表の情報を確認してください。
| 仕様 | 例 |
|---|---|
Polyspace® は、関数の [標準ライブラリ ルーチンの無効な使用] チェックを実行します。このチェックは、sourcePtr または destinationPtr が指すメモリ ブロックが、num を介して割り当てられたメモリ以上のサイズであるかどうかを判定します。 | #include <string.h>
typedef struct {
char a;
int b;
} S;
void func(int);
void main() {
S s;
int d;
memcpy(&d, &s, sizeof(S));
}このコードで、Polyspace は、レッドの [標準ライブラリ ルーチンの無効な使用] エラーを生成します。その理由は次のとおりです。
|
Polyspace は
| #include <string.h>
typedef struct {
char a;
int b;
} S;
void func(int);
void main() {
S s, d={'a',1};
int val;
val = d.b; // val=1
memcpy(&d, &s, sizeof(S));
val = d.b;
// val can have any int value
}このコードでは、Polyspace は、関数 |
ソース引数とコピー先引数が重複する場合、Polyspace はレッドの [標準ライブラリ ルーチンの無効な使用] チェックを報告します。代入の重複は、C 標準で禁止されています。 | 次のメモリ代入にレッド チェックが生成されます。 #include <string.h>
int main() {
char arr[4];
memcpy (arr, arr + 3, sizeof(int));
} |
memset 向けの Polyspace 仕様
構文:
#include <string.h> void * memset ( void * ptr, int value, size_t num );
コードが関数 memset を使用する場合、この表の情報を確認してください。
| 仕様 | 例 |
|---|---|
Polyspace は、関数の [標準ライブラリ ルーチンの無効な使用] チェックを実行します。このチェックは、ptr の指すメモリ ブロックが、num を介して割り当てられたメモリ以上のサイズであるかどうかを判定します。 | #include <string.h>
typedef struct {
char a;
int b;
} S;
void main() {
int val;
memset(&val,0,sizeof(S));
}このコードで、Polyspace は、レッドの [標準ライブラリ ルーチンの無効な使用] エラーを生成します。その理由は次のとおりです。
|
| #include <string.h>
typedef struct {
char a;
int b;
} S;
void main() {
S s;
int val;
memset(&s,0,sizeof(S));
val=s.b; //val=0
}このコードで、 Polyspace は、 |
| #include <string.h>
typedef struct {
char a;
int b;
} S;
void main() {
S s;
int val;
memset(&s,1,sizeof(S));
val=s.b;
// val can have any int value
}このコードで、Polyspace は、
|
