ACSLでメモリの場所を有効にする方法を教えてください。

Question

私は今の問題は、私はRTEのチェックを有効にすると、生成された妥当性チェックが

を証明することができないことであるデバイスは、私が

@ volatile dev->somereg reads somereg_read writes somereg_write; 

を使用してアクセスをモデル化してきたようにこれ

volatile struct mydevice * const dev = (struct mydevice *)MY_DEVICE_ADDRESS; 

にアクセス定義

/*@ assert rte: mem_access: \valid(dev->somereg); */ 

MY_DEVICE_ADDRESS MY_DEVICE_ADDRESS +はsizeof（構造体のmydeviceに）まで有効と見なされるように自分のコードに注釈を付ける方法はありますか？

編集：ここでは

FRAMA-C-WP -wp-RTE -wp-のinit-constの-wpモデル型付きテストで

#include <stdint.h> 

#define MY_DEVICE_ADDRESS (0x80000000) 

struct mydevice { 
    uint32_t somereg; 
    uint32_t someotherreg; 
}; 

volatile struct mydevice * const dev = (struct mydevice *)MY_DEVICE_ADDRESS; 

/*@ axiomatic Physical_Memory { 
    axiom Dev: \valid((struct mydevice*)MY_DEVICE_ADDRESS); 
    } */ 

int main(int argc, const char *argv[]) { 
    //@ assert \valid(dev); 
    //@ assert \false; 
    return 0; 
} 

実行]を動作しない試みです。 c

Answer 1

私は与えられた区間内にポインタを逆参照することであることを示すために、カーネル-absolute-valid-range <min-max>でのオプションがありアサーションが証明しているための唯一の方法は、

/*@ axiomatic Physical_Memory { 
    axiom Dev: \valid((struct mydevice*)MY_DEVICE_ADDRESS); 
    // add more if you have other physical memory accesses 
    } */ 

形の公理ブロックを置くことであると思いますOKですが、EVAだけがそれを利用することができます（これはWPのメモリモデルでは低すぎます）。

WPにオプション-wp-init-constを渡して、グローバルconstの変数が常に初期値と等しいという事実をコンテキストに追加する必要があることを示すことに注意してください。

編集

コメントで述べたように、提案された公理は確かにWPのメモリモデルと矛盾しています。この問題の大部分は、前記モデルにおいて数値アドレス0xnnnnが明らかにshift(global(0),0xnnnn)と定義されているという事実にある。例えば以下に見られるように。 $FRAMAC_SHARE/wp/ergo/Memory.mlw,global(0)は、baseが0であり、したがってshift（これはoffsetのみを変更する）です。 valid_rwの定義は、厳密にはbaseという正の値を課すため、矛盾します。

これはWPのレベルで固定する必要があります。あなたは物理的な場所に記述する必要がない場合は、あなたが公理で\valid_readで\validを置き換えることができます

• ：しかし、新しいFRAMA-Cのリリースを待っている間に利用できるいくつかの回避策があります。モデル内の\valid_readの定義にはbase>0の要件がないため、公理は矛盾につながることはありません。
• あなたは、ソースを修正する余裕がdevextern宣言（またはextern宣言abstract_devに等しいものとしてdevを定義）を作成し、公理に抽象定数を使用することができた場合：この方法で、あなたは平等を持っていません。ロジックモデル内のdev.base==0を削除し、矛盾を削除します。
• 最後に、メモリモデルを$FRAMAC_SHARE/wp/ergo/Memory.mlwにパッチすることができます（そして、あなたの選択に応じて$FRAMAC_SHARE/wp/why3/Memory.whyと$FRAMAC_SHARE/wp/coq/Memory.v）。

 
logic global_base: int 

function global(b: int) : addr = { base = global_base + b; offset = 0 } 

この答えは、これは、他の問題を導入しないことを決して保証で行いもちろんの（注：これを実行する最も簡単な方法は、おそらくのように、globalは抽象ベースに頼る作るだろうモデル）。

Answer 2

私は知っている（私もたくさん試しました）。

私が見つけた唯一の回避策は次のとおりです。

struct mydevice MY_DEVICE_STRUCT; 
volatile struct mydevice * const dev = & MY_DEVICE_STRUCT; 

これは根本的なLLVMが期待するものであるので、あなたがメモリを「インスタンス化」する必要があります。確かに、これを強制的にACSLの表記法で行うとよいでしょう。