acsl

0熱

2答えて

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

私は今の問題は、私はRTEのチェックを有効にすると、生成された妥当性チェックがを証明することができないことであるデバイスは、私が @ volatile dev->somereg reads somereg_read writes somereg_write; を使用してアクセスをモデル化してきたようにこれ volatile struct mydevice * const dev = (stru

frama-c acsl 2017-07-20

---