6

これが私の例です：

int in;
int sum(int n){
    int log_input = n;
    int log_global = in;
    return 0;
}

int main(){
    int n = Frama_C_interval(-10, 10);
    in = n;
    if (n > 0){
        sum(n + 4);
    }
    return 0;
}

私がやりたいのは、メインで初期化されたときに入力変数 n の範囲を見つけて、関数 sum に到達することです。この例の正しい範囲は [1, 10] です。

このサンプルでは、​​元の入力をグローバル値に「保存」し、それを変数log_globalに割り当てて関数 sum に再導入し、関数に到達した元の入力を検出したいと考えています。このサンプルで frama-c を実行すると、log_input の範囲が [5, 14] で、log_global の範囲が [-10, 10] であることがわかります。これが発生する理由を理解しています. inの値はmainの開始時に設定され、nをさらに操作しても影響を受けません。

これをframa-cで変更する簡単な方法があるかどうか疑問に思っていましたか? おそらく、frama-c のコードの単純な変更でしょうか?

私が持っていた無関係なアイデアの 1 つは、メインの if ステートメントを操作することでした。

if (in > 0){
    sum(in + 4);
}

nの代わりにグローバル変数を使用しました。これは確かに正しい範囲になりますが、このソリューションは、より複雑な関数やより深い呼び出しスタックにうまく拡張できません。

4

1 に答える 1

3

これが可能な解決策です。ビルトインFrama_C_interval_splitと適切な-slevel N(ここでは、少なくともN=21) を使用します。関数sumは、N の可能な値ごとに 1 回、N 回検査され、結果は正確になります。

int n = Frama_C_interval_split(-10, 10);

結果：

 [value] Values at end of function sum:
  log_input ∈ [5..14]
  log_global ∈ [1..10]
  __retres ∈ {0}

(基本的に、これは手動のモデル チェックを実行することになるため、N の値が大きい場合、パフォーマンスは良くありません。)

于 2016-02-03T16:37:10.733 に答える