無効アサーション

Question

追加操作用shortとcharデータ型のオーバーフローを確認しながら、FRAMA-Cによって挿入されたアサーションがあるが正しくないと思われる：charの

と短いデータでは正の最大値と負の値は整数データ型です。

この理由は何ですか？

Answer 1

ランクのIntegral型は、算術演算（C11 6.3.1.8通常の算術変換を参照）で使用する場合、intまたはunsignedのいずれかに変換されます。このため、xとyのキャストは(int)になります。デフォルトでは-rteは未定義の動作ではないので、ダウンキャストに対する警告を出さないことに注意してください（6.3.1.3§3は、署名付きダウンキャストがインプリメンテーション定義であり、インプリメンテーションによってシグナルが発生する可能性があることを示します）。あなたはint型に結果を格納する場合、などということ

/*@ assert rte: signed_downcast: (int)x+(int)y ≤ 127; */ 
/*@ assert rte: signed_downcast: -128 ≤ (int)x+(int)y; */ 

注：オプション-warn-signed-downcastを追加する場合は、結果の(char)へのキャストに起因しているあなたは、おそらく探していたアサーションを、表示されますin

ダウンキャスト警告はありません（ただし、署名付きオーバーフロー警告が表示されます）。