保護されていない可能性のある変数
複数のタスク間で共有されるが、タスクによる同時アクセスから保護されていないグローバル変数
説明
保護されていない共有グローバル変数には以下のプロパティがあります。
変数は複数のタスクで使用されている。
Polyspace® により、変数に対する少なくとも 1 つの操作が、他のタスクの操作による割り込みから保護されていないと判定されている。
マルチタスクを対象としていないコードでは、すべてのグローバル変数は非共有です。
検証結果では、これらの変数は [ソース]、[結果のリスト] および [変数アクセス] ペインにおいてオレンジで色付けされています。[ソース] ペインでは、色付けは宣言時にのみ変数に適用されます。
例
#include <limits.h>
int shared_var;
void inc() {
shared_var+=2;
}
void reset() {
shared_var = 0;
}
void task() {
volatile int randomValue = 0;
while(randomValue) {
reset();
inc();
inc();
}
}
void interrupt() {
shared_var = INT_MAX;
}
void interrupt_handler() {
volatile int randomValue = 0;
while(randomValue) {
interrupt();
}
}
void main() {
}この例では、以下のマルチタスキング オプションが指定されている場合、shared_var は保護されていない共有変数です。
| オプション | 値 | |
|---|---|---|
| マルチタスクを手動で構成 |  | |
| タスク |
| |
クリティカル セクションなど、保護メカニズムは指定しません。
演算 shared_var = INT_MAX は shared_var に対する他の演算に割り込み、予期しない動作を発生させる可能性があります。
[結果の詳細] ペインで 
(グラフ) アイコンをクリックすると、2 つの同時実行タスク (スレッド) が表示されます。
1 番目のグラフには、タスクからの変数へのアクセス方法が表示されます。たとえば、タスク interrupt_handler は、共有変数 shared_var に書き込みを行う関数 interrupt を呼び出します。
2 番目のグラフには、タスクの作成方法が表示されます。この例では、main の完了後に両方のタスクが作成されます。場合によっては、main から呼び出された関数内でタスクが作成されることもあります。
#include <stdio.h>
#include <stdlib.h>
#define SIZE_ARRAY 3
typedef unsigned int uint32;
// Defining three functions of which
// only one accesses a global variable
uint32 var;
void Write_to_var(void) {
var+=1;
}
void No_write_read_1(void) {
}
void No_write_read_2(void) {
}
// Defining a 3-element array of function pointers
// that point to the three functions
typedef void (*FuncPtr)(void);
typedef struct {
FuncPtr pFuncPtr;
}FuncPtrStruct;
const FuncPtrStruct FuncPtrArray[SIZE_ARRAY] =
{
{ &Write_to_var },
{ &No_write_read_1 },
{ &No_write_read_2 }
};
void main() {}
// Defining a function that calls one of the three functions
// via the function pointer
void function(int uiSignalType) {
FuncPtrArray[uiSignalType].pFuncPtr();
}
// Entry-point functions in void(void) format for Polyspace analysis
// Analyze this example with
// -D POLYSPACE -entry-points task_10ms,task_20ms,task_50ms
#ifdef POLYSPACE
void task_10ms(void) {
int signalType;
signalType = 0;
function(signalType);
}
void task_20ms(void) {
int signalType;
signalType = 1;
function(signalType);
}
void task_50ms(void) {
int signalType;
signalType = 2;
function(signalType);
}
#endif
この例では、以下のオプションを指定している場合、var は非共有変数として正しく表示されます。
| オプション | 値 | |
|---|---|---|
| マルチタスクを手動で構成 | | |
| タスク |
| |
プリプロセッサ定義 (-D) | POLYSPACE | |
ただし、この変数に関するメッセージは、この変数がタスク task_10ms、task_20ms、task_50ms のいずれかによって書き込まれるか読み取られる可能性があることを示します。
var はタスク task_10ms でのみアクセスされるため、共有変数ではありません。ただし解析では、次の行での近似が原因で、3 つのタスクすべてがこの変数にアクセスしていると報告されます。
FuncPtrArray[uiSignalType].pFuncPtr();
FuncPtrArray は関数ポインターの配列です。インデックス 0 のポインターが指している関数 Write_to_var は、変数 var を更新します。インデックス 1 と 2 のポインターが指している関数 No_write_read_1 と No_write_read_2 は、var には一切アクセスしません。ただし解析では、どの配列アクセスでどの関数が呼び出されるかについての情報は保存されません。その代わり、インデックスに関係なく各配列アクセスが、3 つの関数のいずれか 1 つを呼び出す、という妥当な近似が解析で行われます。この近似の結果、解析ではタスク task_10ms、task_20ms、および task_50ms が関数 Write_to_var、No_write_read_1、No_write_read_2 のそれぞれを呼び出す可能性があると見なされます。別の解析ルートでは、変数が共有されないことが正しく判別されます。
Code Prover は、名前がない共有メモリ領域を検出しません。絶対アドレスをポインターに割り当てたり、動的にメモリを割り当てたりすることで、名前なしメモリ領域が作成される場合があります。こうした領域を表す名前付き変数はありません。
たとえば、次の例では ptr が動的に割り当てられるメモリを指しています。
#include <stdlib.h>
int* ptr;
void flip() {
*ptr = 0;
}
void flop() {
if (*ptr == 0) {
*ptr = 1;
}
}
void main() {
ptr = (int*) malloc(sizeof(int));
}flip() および flop() を指定した場合でも、Code Prover には、ptr (または *ptr) が指すメモリ領域に同時にアクセスできるとは示されません。チェック情報
| 言語: C | C++ |
