問題タブ [acsl]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
frama-c - おそらく無限のC関数のACSL仕様
外部関数の動作、より正確にはそれらの終了を指定しようとしています。ACSLのドキュメントによると、\terminates p;プロパティでは、述語が保持されている場合pは関数が終了することが保証されていますが、保持されていない場合は何も指定されpていません。また、決して返されない関数は次のように指定できることも説明しています。
さらに、ACSLは\exits p;、突然終了した場合の事後条件を指定するプロパティを提供します。だから私は疑問に思っています：
関数が常に無限ループになるように指定しますか？
さらに、仕様は何ですか：
可能な無限ループに関する手段？
c - ACSL - 関数を証明できない
この関数を証明しようとしていますが、無駄です。別の関数も使用していますが、それを証明しました。
誰でも私を助けることができますか？
これまでに書いたコードと仕様は次のとおりです。
bitstring - ACSL ビット列フリック
ACSL 問題について助けが必要です。コンテストは2014-2015年に行われました。これは単なる練習であり、問題が正しく行われたかどうかを確認したいと思います。
ビット文字列フリック:
次の式で x (5 ビット) を解きます。ユニークなソリューションはいくつありますか?
(RCIRC-2(LSHIFT-1 (NOT X)))=00101
解決した後、私はどこにも答えを見つけることができず、賢くて創造的な人々の助けが必要ですが、16のユニークな解決策を得ました!
ありがとう
python - 2013年からの過去のacslプログラムに関するヘルプが必要
私の先生は練習のために古い ACSL プログラムを私たちにやらせています。プログラムは 2013 年のものです。リンクはこちら: https://s3.amazonaws.com/iedu-attachments-question/5a989d787772b7fd88c063aff8393d34_1bee2d300c35eec13edf0a3af515a5a5.pdf
プログラムを開始しましたが、壁にぶつかりました。ここからどうすればよいかわかりません。
誰かヒントを教えてください。Pythonでコーディングしています。
static-analysis - ACSL は、C コードの内部構造体とフィールドに注釈を「割り当て」ます
次のようなデータ構造があるとします。
次の例では、Frama-C が C 型の構造体のフィールドの場所を割り当てていないようです。
上記の注釈は Frama-C でまったく受け入れられますか?
コードは次のように精緻化されます。主な目標は、フィールド C_Field を 0 にリセットすることです。
関数 Reset の契約は満たされていますが、関数 Initialize の契約は満たされていません。Initialize のコントラクトに正しい「assigns」を記述する方法は?
frama-c - ACSLでメモリの場所を強制的に有効にする方法は?
デバイスアクセスを次のように定義します
を使用してアクセスをモデル化しました
問題は、RTE チェックを有効にすると、生成された有効性チェックを証明できないことです。
MY_DEVICE_ADDRESS + sizeof(struct mydevice) までの MY_DEVICE_ADDRESS が有効と見なされるように、コードに注釈を付ける方法はありますか?
編集：これはうまくいかない試みです
で実行
frama-c-wp -wp-rte -wp-init-const -wp-model 型付き test.c