Frama-cスライス：プラグマctrlを取得するためのエントリを選択

Question

CTRLスライスの取得に問題があります。

私はこれを実行して、OpenSSLを分析しようとしている：

コードは何も生じない

int dtls1_process_heartbeat(SSL *s) 

    { 
    unsigned char *p = &s->s3->rrec.data[0], *pl; 
    unsigned short hbtype; 
    unsigned int payload; 
    unsigned int padding = 16; /* Use minimum padding */ 
    /* Read type and payload length first */ 
    hbtype = *p++; 
    n2s(p, payload); 
    pl = p; 

    if (s->msg_callback) 
      s->msg_callback(0, s->version, TLS1_RT_HEARTBEAT, 
        &s->s3->rrec.data[0], s->s3->rrec.length, 
        s, s->msg_callback_arg); 

    if (hbtype == TLS1_HB_REQUEST) 
      { 
      unsigned char *buffer, *bp; 
      int r; 

      /* Allocate memory for the response, size is 1 byte 
      * message type, plus 2 bytes payload length, plus 
      * payload, plus padding 
      */ 
      buffer = OPENSSL_malloc(1 + 2 + payload + padding); 
      bp = buffer; 

      /* Enter response type, length and copy payload */ 
      *bp++ = TLS1_HB_RESPONSE; 
      s2n(payload, bp); 
      /*@ slice pragma stmt; */ 
      memcpy(bp, pl, payload); 
      bp += payload; 
      /* Random padding */ 
      RAND_pseudo_bytes(bp, padding); 
      r = dtls1_write_bytes(s, TLS1_RT_HEARTBEAT, buffer, 3 + payload + padding); 

      if (r >= 0 && s->msg_callback) 
        s->msg_callback(1, s->version, TLS1_RT_HEARTBEAT, 
          buffer, 3 + payload + padding, 
          s, s->msg_callback_arg); 

      OPENSSL_free(buffer); 

      if (r < 0) 
        return r; 
      } 
    else if (hbtype == TLS1_HB_RESPONSE) 
      { 
      unsigned int seq; 

      /* We only send sequence numbers (2 bytes unsigned int), 
      * and 16 random bytes, so we just try to read the 
      * sequence number */ 
      n2s(pl, seq); 

      if (payload == 18 && seq == s->tlsext_hb_seq) 
        { 
        dtls1_stop_timer(s); 
        s->tlsext_hb_seq++; 
        s->tlsext_hb_pending = 0; 
        } 
      } 

    return 0; 
    } 

`

frama-c ./ssl/d1_both.c -main dtls1_process_heartbeat -slice-calls memcpy -cpp-command "gcc -C -E -I ./include/ -I ./" -then-on 'Slicing export' -print 

以下のようなものですので、私は、この試みた：希望を逆方向スライスを得るために

frama-c ./ssl/d1_both.c -main dtls1_process_heartbeat -slice-pragma dtls1_process_heartbeat -cpp-command "gcc -C -E -I ./include/ -I ./" -then-on 'Slicing export' -print 

しかし、私はまだその

void dtls1_process_heartbeat(void); 

    void dtls1_process_heartbeat(void) 
    { 
     return; 
    } 

のような何を取得するにはどうすればそのようなスライスを得ることができますか？

function A(){ 
… 

memcpy() 
... 

} 


function B(){ 
… 
… 
... 

} 

function C(){ 
… 

memcpy() 

... 

} 

私はmemcpy()で行うためにすべてをキャプチャしたいので、私はAとCを維持したいが、私はエントリポイントを選択する必要がありませんB.

どのように？プラグマを選ぶには？

私は私の質問を明確に述べたことを願っています。私は数日間混乱させてしまった。

Answer 1

まず、Frama-Cフッ素は廃止されたバージョンであることに注意してください。 3年以上前にリリースされています。いくつかのスライシング関連のバグが修正されました。より新しいバージョン、好ましくはAluminiumにアップグレードしてください。

第二に、オプション-slicing-valueのドキュメントが

は、左の値V1の結果を選択している、...、VNエントリポイントとして与えられた関数の 終わりに（アドレスが で評価されていますエントリとして与えられた機能の開始 ポイント

あなたが望むことはほとんどありません。 -slice-callsのオプション、もっと正確には-slice-calls memcpyを試しましたか？

Bは、memcpyの呼び出しで後で使用される値を計算する場合、スライスに保持されることに注意してください。