2

Frama-Cでは、基本型のサイズを自由に指定することはできますか?

私のターゲットである TMS320F2808 DSP には 16 ビットのバイトがあります。char、short、int 型はすべて 1 バイトで、long 型は 2 バイトです。

Frama-C にこれらのサイズを指定する方法が、可能であればまだわかりません。

4

2 に答える 2

2

あなたはすでにオプションを発見しているかもしれません-machdep。コマンドframa-c -machdepはリストを表示します:

$ frama-c -machdep help
[kernel] supported machines are x86_64 x86_32 ppc_32 x86_16.

残念ながら、の値はCHAR_BITmachdep パラメータの 1 つではありません。代わりに、値 8 は Frama-C for の多くの場所でハードコーディングされていCHAR_BITます。8 of より大きい値のサポートを追加するのCHAR_BITは簡単ですが、反復的なプログラミング タスクです。単純にこれらすべての場所を特定し、Bit_utils.sizeofchar()代わりに使用するように変更する必要があります。実際、誰かがすでにこれを行っているので、間違いなく実行可能ですが、その変更が Frama-C の開発に反映されることはありませんでした (オープンソース ソフトウェアの世界へようこそ)。

CHAR_BIT == 16以上のことを行えば、 、sizeof(int) == 1で新しいアーキテクチャを作成するのsizeof(long) == 2は比較的簡単な操作になります。

変更方法

以下のコマンドを使用して、潜在的な変更サイトの最初のリストを取得します。これは、番号 のすべての出現を検索します8。

$ grep -rI \\W8\\W src/*/*.ml
src/ai/base.ml: 8 (* FIXME: CHAR_BIT *), (String.length s)
src/aorai/aorai_register.ml: (* ステップ 8 : 情報が削除されたテーブルのクリア
src/aorai/ltllexer.ml: | 8 ->
src/aorai/promelalexer.ml: | 8 ->
src/aorai/promelalexer_withexps.ml: | 8 ->
src/aorai/yalexer.ml: | 8 ->
src/gui/design.ml: 高さ * 8 / 5 (* 16/10 の比率 *)
src/gui/gtk_form.ml: val テーブル = GPack.table ~rows:2 ~col_spacings:8 ~packing ()
src/gui/gtk_helper.ml: ~fallback:"#UTF-8 でもロケールでも ISO-8859-15 でもありません#"
src/gui/gtk_helper.ml: ~to_codeset:"UTF-8"
src/gui/source_manager.ml:(* ソースファイルを UTF-8 またはロケールとして変換してみてください。 *)
src/kernel/stmts_graph.ml: | ブロック _ -> [`Shape `Box; `フォントサイズ 8]
src/lib/binary_cache.ml:let cache_size () = 1 lsl (8 + MemoryFootprint.get ())
src/lib/bitvector.ml: ba [I 8] の場合
src/logic/description.ml: | IPPredicate(kind,kf,ki,_) -> [I 8;F kf;K ki] @ kind_order 種類
src/logic/property.ml: Hashtbl.hash (8, Kf.hash f, Kinstr.hash ki, hash_bhv_loop b)
src/logic/property_status.ml: | Never_tried -> [`Style `Bold; `幅 0.8 ]
src/memory_state/offsetmap.ml: char_width = 8 in
src/misc/bit_utils.ml: Int_Base.inject (Int.of_int (warn_if_zero ty (bitsSizeOf ty) / 8))
src/pdg/ctrlDpds.ml: (2) if (c) (3) y = 3; (4) 後藤 L; そうでなければ (5) z = 8;
src/pdg/ctrlDpds.ml: (8) L : x を返します。
src/pdg/ctrlDpds.ml: (1) -> (2) -> (6) -> (8)
src/printer/cil_printer.ml: Integer.pred (Integer.of_int (8 * (Cil.bytesSizeOfInt k)))
src/printer/cil_printer.ml: CompoundInit (_, il) when List.length il >= 8 -> true
src/project/state_builder.ml: debug ~level:8 "updating" p;
src/value/builtins_nonfree.ml: Value_parameters.debug "%a の find_ival(8) は %a を返します"
src/value/builtins_nonfree.ml:let int_hrange = Int.two_power_of_int (8 * Cil.theMachine.Cil.theMachine.sizeof_int -1)
src/value/builtins_nonfree_print_c.ml: let step = if iso then 1 else (Integer.to_int modu) / 8 in
src/value/builtins_nonfree_print_c.ml: let start = ref ((Integer.to_int bk) / 8) in
src/value/builtins_nonfree_print_c.ml: let ek = ek / 8 in
src/value/eval_exprs.ml: let offs_bytes = fst (Cil.bitsOffset typ_exp offs) / 8 in
src/value/eval_terms.ml: [i * 8 * sizeof( *tlv)] *)
src/value/value_parameters.ml: (デフォルトは 8; 実験的)"
src/wp/Cint.ml: in let hsb p = let n = p lsr 8 in if n = 0 then hsb.(p) else 8 + hsb.(n)
src/wp/GuiPanel.ml: let options = GPack.hbox ~spacing:8 ~packing () in
src/wp/GuiPanel.ml: let control = GPack.table ~columns:4 ~col_spacings:8 ~rows:2 ~packing () in
src/wp/Matrix.ml: let buffer = Buffer.create 8 in
src/wp/cil2cfg.ml: | VblkIn (Bloop s,_) -> (8, s.sid)
src/wp/ctypes.ml: | 8 -> 署名されている場合は SInt64、そうでない場合は UInt64
src/wp/ctypes.ml: | 8 -> Float64
src/wp/ctypes.ml: | サイズ -> WpLog.not_yet_implemented "%d-bits floats" (8*サイズ)
src/wp/ctypes.ml: let m = Array.create 8 になし
src/wp/ctypes.ml: (Cil.bitsSizeOf ctype / 8)
src/wp/ctypes.ml: (Cil.bitsSizeOf ctype / 8)
src/wp/driver.ml: | 8 ->
src/wp/rformat.ml: | 8 ->
src/wp/script.ml: | 8 ->

1 つ目は明らかに真陽性で、2 つ目は明らかに偽陽性です。最初のケースでは、コンテキストは type の値を期待していますint。最も単純な変更は次のとおりです。

インデックス: src/ai/base.ml
================================================== =================
--- src/ai/base.ml (リビジョン 24517)
+++ src/ai/base.ml (作業コピー)
@@ -116,7 +116,7 @@
   u、l =
     と一致する
     | | CSString s ->
- 8 (* FIXME: CHAR_BIT *), (String.length s)
+ bitsSizeOf charType, (String.length s)
     | | CSWstring s ->
    bitsSizeOf theMachine.wcharType, (List.length s)
   の

上記のリストでは、パターンCil.bitsSizeOf … / 8は が を8表していることを示しCHAR_BITていますが、それ以外の場合は、ソース コードを見て意図を理解する必要があります。

難しさは、定数 8 がとる可能性のあるさまざまな形式に由来します。8Lまた、同じ定数であるがタイプが である に遭遇する場合もありint64ます。その定数が char の幅を表す場合は、 に置き換えることができますInt64.of_int (bitsSizeOf charType)。src/ai/base.ml に 1 つあります。

インデックス: src/ai/base.ml
================================================== =================
--- src/ai/base.ml (リビジョン 24517)
+++ src/ai/base.ml (作業コピー)
@@ -156,12 +156,12 @@
     (楽しい_x ->
        Scanf.sscanf x "%Li-%Li" を試す
          (楽しい最小最大 ->
- let mul8 = Int64.mul 8L in
+ let mul_CHAR_BIT = Int64.mul (Int64.of_int (bitsSizeOf charType)) in
             MinValidAbsoluteAddress.set
- (Abstract_interp.Int.of_int64 (mul8 分));
+ (Abstract_interp.Int.of_int64 (mul_CHAR_BIT 分));
             MaxValidAbsoluteAddress.set
               (Abstract_interp.Int.of_int64
- (Int64.pred (mul8 (Int64.succ max)))))
+ (Int64.pred (mul_CHAR_BIT (Int64.succ max)))))
        End_of_file | Scanf.Scan_failure _ | 失敗 _ as e ->
          Kernel.abort "Invalid -absolute-valid-range integer-integer: 各整数は 10 進数、16 進数 (0x、0X)、8 進数 (0o)、または 2 進数 (0b) 表記で、64 ビットで保持する必要があります。正しい例絶対有効範囲は 1 ～ 0xFFFFFF0 です。@\nエラーは %S@ でした。"
            (Printexc.to_string e))

ただし、この最後の変更を行うと、コマンドライン オプションが使用されたときに Frama-C がクラッシュします-absolute-valid-range。これは、現在初期化されている順序のためです (フロントエンドはchar、コマンドライン引数が解釈される時点でのサイズに関する質問に答える準備ができていません)。 ）。そのため、この特定の変更は延期する必要があり、Frama-C が少し再構築されるまで、オプションは引き続き 8 ビット文字を想定することに注意する必要があります。

と とは別にint、int64Frama-C は多精度 (割り当て) 整数も使用します。そのタイプの定数 8 は、通常、 として見つかりますInt.eight。Bit_utils.sizeofcharこの関数は多倍長整数を返すため、これを の呼び出しに置き換えることができます。コードは、3 によるシフトについても検査する必要があります。

于 2013-11-20T23:34:09.867 に答える