Strumento generale di verifica driver statico e limitazioni tecniche

SDV presenta le limitazioni generali seguenti:

• SDV verifica un solo driver alla volta e il driver deve seguire uno di questi modelli di driver da verificare completamente: WDM, KMDF, NDIS o Storport. Per altre informazioni sui driver supportati, vedere Determinare se il driver statico verifica supporta il driver o la libreria.

• I driver che non rientrano in una delle categorie precedenti saranno gravemente limitati nelle regole che possono essere verificati e sono più probabilità di non riuscire durante l'analisi.

• Il file di progetto del driver e il codice sorgente devono risiedere nel computer locale. Non è possibile verificare i driver in remoto.

• SDV viene installato con le impostazioni locali inglese (Stati Uniti). Di conseguenza, gli elementi dipendenti dalle impostazioni locali, ad esempio la formattazione delle stringhe, usano le varianti inglesi (Stati Uniti). Questa limitazione è presente anche quando SDV è installato in versioni localizzate di Windows diverse dall'inglese (Stati Uniti).

Il motore di verifica SDV presenta limitazioni tecniche che impediscono di interpretare correttamente il codice del driver. In particolare, il motore di verifica:

• Non riconosce che gli interi a 32 bit sono limitati a 32 bit. Di conseguenza, non rileva errori di overflow o sottoflow.

• Assicurarsi che i driver che dichiarano i punti di ingresso con la parola chiave statica vengano elaborati correttamente. Tuttavia, per assicurarsi che i punti di ingresso statici siano riconosciuti, SDV ha richiesto una modifica ai file Sdv-map.h per le funzioni statiche: ad esempio, se si dichiara un punto di ingresso statico:

  static DRIVER_UNLOAD Unload;
  

  Sdv-map.h non conterrà la voce consueta per fun_DriverUnload.

  #define fun_DriverUnload Unload
  

  Si noterà invece che il nome della funzione è mangled:

    #define fun_DriverUnload sdv_static_function_Unload_1
  

  Ciò è necessario perché più moduli potrebbero avere una funzione statica denominata Scarica. Il nome è mangled per evitare potenziali conflitti.

• Impossibile interpretare le funzioni di callback del driver o di invio driver definite in un driver di esportazione in cui il driver di esportazione ha un file di definizione del modulo (.def) che nasconde la funzione di invio del driver. Per evitare questo problema, aggiungere la funzione di invio driver alla sezione EXPORT del file module-definition (.def).

• Impossibile rilevare correttamente il tipo di ruolo di una funzione se i riferimenti seguenti a questa funzione non si trovano nella stessa unità di compilazione.

  • Dichiarazione della funzione.
  • Definizione della funzione.
  • Assegnazione della funzione a un punto di ingresso del driver o a una funzione di callback.

  L'unità di compilazione viene definita qui come il set più piccolo di file di codice sorgente e altri file di origine inclusi in questo file di codice sorgente.

  Se un tipo di ruolo di funzione non viene rilevato da SDV, SDV non verificherà le tracce che provengono da questa funzione.

  Ad esempio, se un driver definisce (o implementa) una funzione EvtDriverDeviceAdd nel file mydriver.c. Questa unità di compilazione (o qualsiasi file con estensione h inclusa da mydriver.c) deve contenere la dichiarazione del tipo di ruolo della funzione per la funzione EvtDriverDeviceAdd .

• Non interpreta la gestione delle eccezioni strutturate. Per istruzioni try/except , SDV analizza la sezione protetta come se non venga generata alcuna eccezione. Non analizza l'espressione o il codice del gestore delle eccezioni.

  // The try/except statement
  __try 
  {
     // guarded section
  }
  __except ( expression )
  {
     // exception handler
  } 
  

  Per le istruzioni try/final , SDV analizza la sezione protetta e quindi il gestore di terminazione, come se non venga generata alcuna eccezione.

  // The try/finally statement
  __try {
     // guarded section
  }
  __finally {
     // termination handler
  }
  

  Per entrambe le istruzioni try/except e try/final , SDV ignora l'istruzione leave .

  Per entrambe le istruzioni try/except e try/final , un salto fuori dal blocco try impedisce l'analisi delle istruzioni tranne o infine . Per informazioni su come riscrivere in modo che sia possibile usare un'istruzione leave, vedere l'argomento relativo all'avviso del compilatore C6242.

• Ignora l'aritmetica del puntatore. Ad esempio, mancherà situazioni in cui un puntatore viene incrementato o decrementato. Questa limitazione può causare risultati falsi negativi e falsi positivi.

• Ignora le unioni. Nella maggior parte dei casi, un'unione viene considerata come struct e ciò potrebbe comportare falsi positivi o falsi negativi.

• Ignora le operazioni di cast, quindi perderà entrambi gli errori risolti dalla recasting e dagli errori causati dal cast. Ad esempio, il motore presuppone che un intero recast come carattere abbia ancora il valore integer.

• Inizializza solo le matrici che sono matrici di puntatori di funzione. SDV genera un avviso e comprime l'inizializzatore della matrice ai primi 1000 elementi. Per altri tipi di matrice, viene inizializzato solo il primo elemento.

• I costruttori di oggetti inizializzati nelle matrici non vengono chiamati. Nel frammento di codice seguente, ad esempio, x non viene impostato su 10 perché SDV non chiama il costruttore.

  class A
  {
  public:
      A() {
        x = 10;
      }
  
      int x;
  };
  
  void main()
  {
      A a[1];
  }
  

• SDV non supporta l'uso dei costruttori per inizializzare le matrici. Nel frammento di codice seguente, ad esempio, il costruttore per P non verrà chiamato correttamente nella funzione principale e non inizializzerà l'elemento nella matrice p2:

  class P
  {
  public:
      P() : x(0) {}
      int x;
  };
  
  void main()
  {
      P* p1 = new P[1];
  
      P p2[1] = {P()};
  }
  

• SDV ignora le intestazioni precompilate. I driver che usano intestazioni precompilate solo per velocizzare la compilazione verranno compilati più lentamente con SDV. I driver che devono usare intestazioni precompilate per la compilazione riuscita non verranno compilati con SDV.

• Impossibile dedurre alcuni tipi di assegnazioni implicite effettuate tramite chiamate a RtlZeroMemory o NdisZeroMemory. Il motore esegue un'analisi ottimale per inizializzare la memoria su zero, ma solo quando può identificare il tipo. Di conseguenza, il codice che dipende da queste funzioni per inizializzare la memoria potrebbe generare falsi difetti lungo alcuni percorsi di codice.

• Non supporta un modello di memoria che consente di tenere traccia dell'invio manuale delle richieste di I/O a un driver KMDF. Il motore supporta solo i metodi che si basano sul framework per recapitare le richieste di I/O al driver (per l'invio sequenziale o parallelo).

• Non supporta l'uso del tipo di dati float per i confronti. Questa limitazione tecnica può produrre risultati falsi negativi e falsi positivi.

• SDV non supporta l'ereditarietà virtuale o le funzioni virtuali. SDV non genera difetti che seguono un percorso di codice tramite funzioni virtuali, che potrebbero causare la perdita di veri difetti. L'ereditarietà virtuale viene considerata come ereditarietà regolare, che potrebbe causare falsi difetti o perdere veri difetti.