Partager via

Outil général et limitations techniques du vérificateur de pilote statique

  • Article

SDV présente les limitations générales suivantes :

  • SDV vérifie un seul pilote à la fois et le pilote doit suivre l’un de ces modèles de pilotes pour être entièrement vérifié : WDM, KMDF, NDIS ou Storport. Pour plus d’informations sur les pilotes pris en charge, consultez Déterminer si Static Driver Verifier prend en charge votre pilote ou bibliothèque.

  • Les pilotes qui ne appartiennent pas à l’une des catégories ci-dessus seront fortement limités dans les règles qui peuvent être vérifiées et sont plus susceptibles d’échouer pendant l’analyse.

  • Le fichier projet du pilote et le code source doivent résider sur l’ordinateur local. Vous ne pouvez pas vérifier les pilotes à distance.

  • SDV est installé avec les paramètres régionaux anglais (États-Unis). Par conséquent, les éléments dépendant des paramètres régionaux, tels que la mise en forme de chaîne, utilisent les variantes anglaises (États-Unis). Cette limitation est présente même lorsque SDV est installé sur des versions localisées de Windows autres que l’anglais (États-Unis).

Le moteur de vérification SDV présente des limitations techniques qui l’empêchent d’interpréter correctement un code de pilote. Plus précisément, le moteur de vérification :

  • Ne reconnaît pas que les entiers 32 bits sont limités à 32 bits. Par conséquent, il ne détecte pas les erreurs de dépassement de capacité ou de sous-flux.

  • Vérifie que les pilotes qui déclarent leurs points d’entrée avec les mot clé statiques sont traités correctement. Toutefois, pour s’assurer que les points d’entrée statiques sont reconnus, SDV nécessitait une modification des fichiers Sdv-map.h pour les fonctions statiques : par exemple, si vous déclarez un point d’entrée statique :

    static DRIVER_UNLOAD Unload;

    Le fichier Sdv-map.h ne contiendra pas l’entrée habituelle pour fun_DriverUnload.

    #define fun_DriverUnload Unload

    Au lieu de cela, vous voyez que le nom de la fonction est mangle :

      #define fun_DriverUnload sdv_static_function_Unload_1

    Cela est nécessaire, car plusieurs modules peuvent avoir une fonction statique nommée Unload. Le nom est mangle pour éviter les conflits potentiels.

  • Impossible d’interpréter les fonctions de distribution du pilote ou de rappel de pilote définies dans un pilote d’exportation où le pilote d’exportation a un fichier de définition de module (.def) qui masque la fonction de répartition du pilote. Pour éviter ce problème, ajoutez la fonction de répartition du pilote à la section EXPORTS du fichier de définition de module (.def).

  • Impossible de détecter correctement le type de rôle d’une fonction si les références suivantes à cette fonction ne se trouvent pas dans la même unité de compilation.

    • Déclaration de la fonction.
    • Définition de la fonction.
    • Affectation de la fonction à un point d’entrée de pilote ou à une fonction de rappel.

    L’unité de compilation est définie ici comme le plus petit ensemble de fichiers de code source et d’autres fichiers sources inclus dans ce fichier de code source.

    Si aucun type de rôle de fonction n’est détecté par SDV, SDV ne vérifie pas les traces qui proviennent de cette fonction.

    Par exemple, si un pilote définit (ou implémente) une fonction EvtDriverDeviceAdd dans le fichier mydriver.c. Cette unité de compilation (ou tous les fichiers .h inclus dans mydriver.c) doit contenir la déclaration de type de rôle de fonction pour la fonction EvtDriverDeviceAdd .

  • N’interprète pas la gestion structurée des exceptions. Pour les instructions try/except , SDV analyse la section protégée comme si aucune exception n’était levée. N’analyse pas l’expression ou le code du gestionnaire d’exceptions.

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

    Pour les instructions try/finally , SDV analyse la section protégée, puis le gestionnaire de terminaison, comme si aucune exception n’était levée.

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

    Pour les instructions try/except et try/finally , SDV ignore l’instruction leave .

    Pour les instructions try/except et try/finally , un saut en dehors du bloc try empêche l’analyse des instructions except ou finally . Pour plus d’informations sur la façon de réécrire afin de pouvoir utiliser une instruction leave, consultez la rubrique sur l’avertissement du compilateur C6242.

  • Ignore l’arithmétique du pointeur. Par exemple, il manque des situations dans lesquelles un pointeur est incrémenté ou décrémenté. Cette limitation peut entraîner des résultats faux négatifs et faux positifs.

  • Ignore les unions. Dans la plupart des cas, une union est traitée comme un struct , ce qui peut entraîner des faux positifs ou des faux négatifs.

  • Ignore les opérations de cast, de sorte qu’il manque à la fois les erreurs qui sont résolues par la rediffusion et les erreurs qui sont provoquées par le cast. Par exemple, le moteur part du principe qu’un entier qui est rediffusé en tant que caractère a toujours la valeur entière.

  • Initialise uniquement les tableaux qui sont des tableaux de pointeurs de fonction. SDV émet un avertissement et compresse l’initialiseur de tableau sur les 1 000 premiers éléments. Pour les autres types de tableau, seul le premier élément est initialisé.

  • Les constructeurs d’objets initialisés dans des tableaux ne sont pas appelés. Par exemple, dans l’extrait de code suivant, x n’est pas défini sur 10, car SDV n’appelle pas le constructeur.

    class A
{
public:
    A() {
      x = 10;
    }

    int x;
};

void main()
{
    A a[1];
}

  • SDV ne prend pas en charge l’utilisation de constructeurs pour initialiser des tableaux. Par exemple, dans l’extrait de code suivant, le constructeur pour P n’est pas appelé correctement dans la fonction main et n’initialise pas l’élément dans le tableau p2 :

    class P
{
public:
    P() : x(0) {}
    int x;
};

void main()
{
    P* p1 = new P[1];

    P p2[1] = {P()};
}

  • SDV ignore les en-têtes précompilés. Les pilotes qui utilisent des en-têtes précompilés uniquement pour accélérer la compilation seront compilés plus lentement avec SDV. Les pilotes qui doivent utiliser des en-têtes précompilés pour une compilation réussie ne seront pas compilés avec SDV.

  • Impossible de déduire certains types d’affectations implicites effectuées par le biais d’appels à RtlZeroMemory ou NdisZeroMemory. Le moteur effectue une analyse du mieux possible pour initialiser la mémoire à zéro, mais uniquement lorsqu’il peut identifier son type. Par conséquent, le code qui dépend de ces fonctions pour initialiser la mémoire peut générer de faux défauts le long de certains chemins de code.

  • Ne prend pas en charge un modèle de mémoire qui lui permettrait de suivre la distribution manuelle des demandes d’E/S à un pilote KMDF. Le moteur prend uniquement en charge les méthodes qui s’appuient sur l’infrastructure pour remettre les demandes d’E/S au pilote (pour la répartition séquentielle ou parallèle).

  • Ne prend pas en charge l’utilisation du type de données float pour les comparaisons. Cette limitation technique peut produire des résultats faux négatifs et faux positifs.

  • SDV ne prend pas en charge l’héritage virtuel ou les fonctions virtuelles. SDV ne génère pas de défauts qui suivent un chemin de code via des fonctions virtuelles, ce qui peut entraîner la perte de vrais défauts. L’héritage virtuel est traité comme un héritage normal, ce qui peut entraîner de faux défauts ou perdre de vrais défauts.