Frama-c Slice: Wählen Sie einen Eintrag, um Pragma Ctrl

Question

Ich habe ein Problem, ein CTRL-Slice zu bekommen.

Ich versuche, OpenSSL zu analysieren, indem das Lauf:

der Code ist wie unten

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 

, die nichts produziert, also versuchte ich dann dies: wollen um ein Vorwärts-Schneiden zu erhalten

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 

Aber ich immer noch nichts, wie die

void dtls1_process_heartbeat(void); 

    void dtls1_process_heartbeat(void) 
    { 
     return; 
    } 

Wie kann ich ein Stück wie das?

function A(){ 
… 

memcpy() 
... 

} 


function B(){ 
… 
… 
... 

} 

function C(){ 
… 

memcpy() 

... 

} 

Ich will alles erfassen mit memcpy() zu tun, so möchte ich A und C halten, aber nicht B.

Wie soll ich einen Einstiegspunkt wählen? Wie wähle ich das Pragma?

Ich hoffe, ich habe meine Frage klar formuliert; Es hat mich tagelang verwirrt.

Answer 1

Beachten Sie, dass Frama-C Fluorine eine veraltete Version ist. Es wurde vor mehr als 3 Jahren veröffentlicht. Einige Slicing-Bugs wurden in der Mitte behoben. Bitte aktualisieren Sie auf eine neuere Version, vorzugsweise Aluminium.

Zweitens ist die Dokumentation für die Option -slicing-value ist

das Ergebnis der linken Wert v1 wählen, ..., vn am Ende der Funktion als Einstiegspunkt angegeben (Adressen werden bei der Auswertung Anfang der Funktion als Eintrag Punkt)

Es ist unwahrscheinlich, zu tun, was Sie wollen. Haben Sie versucht, die Option -slice-calls, genauer -slice-calls memcpy?

Denken Sie auch daran, dass B im Slice beibehalten wird, wenn er einen Wert berechnet, der später innerhalb eines Aufrufs an memcpy verwendet wird.