Brevet FR2838205A1 — publié le 20031010

PROCEDE DE DETECTION D'ERREURS DANS UN PROGRAMME INFORMATIQUE La présente invention concerne un procédé de détection d'erreurs dans un programme informatique. Ce procédé peut être utilisé, soit pour détecter des erreurs dans le code d'un programme informatique existant, soit pour éviter l'introduction d'erreurs dans un programme informatique en cours de développement. Plus précisément, l'invention vise un procédé statique de détection des erreurs de programmation, c'est-à-dire par analyse du code source du programme informatique, par opposition aux procédés dynamiques de détection d'erreurs qui détectent des erreurs de programmation lors de l'exécution du programme. On connaît, par l'article de Dawson Engler intitulé "Checking system rules using sytem-specific programmer-written compiler extensions" OSDI, 2000, un procédé, appelé xg++, de détection d'erreurs de programmation dans un programme informatique. Ce procédé comporte une première étape de représentation du programme informatique sous forme de graphe du flot de contrôle (en anglais "Control Flow Graph", CFG). Ce graphe est constitué de flèches et de n#uds, les flèches représentant des transitions entre des instructions du programme informatique représentées par les noeuds. Le graphe du flot de contrôle CFG peut être obtenu en compilant le code source du programme informatique P, par exemple avec le compilateur GNU C. Dans la suite de la description, et par souci de simplification, on utilisera indifféremment l'instruction informatique et le n#ud associé à cette instruction dans le graphe CFG. Le procédé xg++ comporte une deuxième étape de description des instructions du programme informatique en utilisant un ensemble limité de patrons (en anglais "patterns") prédéfinis. Toutefois, ce procédé ne permettant pas à l'utilisateur de définir d'autres patrons appropriés à modéliser une instruction ou une transition du programme informatique, il est d'utilisation très complexe. En outre, ces patrons permettent seulement une analyse syntaxique des instructions du programme, et non leur analyse sémantique. La Demanderesse, cherchant à simplifier et à augmenter l'efficacité de la détection statique d'erreurs de programmation, a recherché une méthode de modélisation, tant syntaxique que sémantique, de tout type d'instruction informatique. Dans un domaine distinct de celui de la détection d'erreurs de programmation, à savoir, le domaine de la reconnaissance du langage naturel, il existe une façon de représenter des phrases, en utilisant un modèle syntaxique et sémantique appelé "psi-terme" (en anglais "psiterm"). Les psi-termes sont définis dans l'article de Hassan Aït-Kaci intitulé "An Overview of LIFE" in : Joachim W. Schmidt, Anatoly A. Stogny (Eds. ): Next Generation Information System Technology, First International EastMlest Data Base Workshop, Kiev, USSR, October 9-12, 1990, Proceedings Lecture Notes in Computer Science, Vol. 504, Springer, 1991, ISBN 3-540- 54141-1, pp. 42-58". Les psi-termes sont des généralisations des termes logiques de premier ordre, les termes logiques de premier ordre étant des expressions de l'une des formes suivantes : - constante : a, 2, "string" ; -variable : X, Y, ; ou - terme composé : f (a), g (X), h (f(X), "string"). Les termes logiques de premier ordre ne permettent pas de modéliser, en utilisant un seul terme logique de premier ordre, les instructions informatiques complexes, comme par exemple l'instruction x = x + 2. Un avantage fondamental des psi-termes par rapport à ces termes logiques de premier ordre est qu'ils permettent de représenter toute instruction informatique avec un seul psi-terme. Par exemple, l'instruction informatique x = x + 2 peut être représentée par le psi-terme unique suivant : modify~expr( type => Int:integer~type, op~0 => X:var~decl(name => identifier~node(strg=>"x")), op~1 => plus~expr( type=>lnt, op~0 => X, op~1 => integer~cst (high =>0, low =>2))) L'invention vise ainsi à résoudre le problème de la détection d'erreurs dans un programme informatique représenté sous forme d'un graphe du flot de contrôle, en modélisant les instructions de ce programme au moyen des psi-termes. La présente invention a plus particulièrement pour objet un procédé de recherche d'au moins une instruction cible dans un programme informatique représenté sous forme d'un graphe comportant des transitions entre des instructions du programme informatique, le procédé comportant : -une étape de modélisation de l'instruction cible par au moins un modèle de type psi-terme ; -une étape de parcours d'un sous-graphe du graphe à partir d'au moins une instruction source, en testant pour chaque instruction parcourue dans le sous-graphe, si l'instruction parcourue est conforme au modèle de l'instruction cible. Conformément à la présente invention, toute instruction cible peut être modélisée en utilisant un seul psi-terme. Outre l'avantage de concision, l'utilisation des psi-termes apporte un gain très significatif en flexibilité et en puissance d'expression. D'une part, la flexibilité est améliorée du fait que les modèles du type psi-termes ne sont pas construits à partir d'un nombre limité de modèles prédéfinis, mais sont définis directement à partir d'un arbre syntaxique généré pour chaque instruction du programme lors de sa compilation. Cela permet de définir des modèles correspondant à des arbres syntaxiques ou des fragments d'arbres quelconques et donc, de modéliser, sans limitation, des familles complexes d'instructions. D'autre part, la puissance d'expression est considérablement accrue par la possibilité d'inclure des contraintes dans les modèles du type psitermes. On peut ainsi définir des modèles qui décrivent à la fois la structure syntaxique des instructions modélisées et le contexte sémantique de leur apparition. Par exemple, le psi-terme suivant permet de modéliser toutes les utilisations d'une variable X qui contiennent le résultat d'un appel de fonction préalable : X :var~decl # reaching~def(X)=call~expr Ce modèle utilise une fonction "reaching~def(X)" qui, pour toute variable, retourne l'instruction dans le programme qui a affecté cette variable pour la dernière fois. Une telle information est calculée par tout compilateur ; les contraintes dans les psi-termes constituent donc un moyen très approprié pour exploiter toutes les informations sémantiques internes au compilateur. Le parcours du graphe du flot de contrôle s'effectue à partir d'un ensemble quelconque de n#uds du graphe, par exemple, à partir du n#ud associé au point d'entrée du programme informatique. Pour chaque n#ud parcouru, on vérifie si l'instruction associée à ce n#ud est conforme au modèle de l'instruction cible, par exemple en déterminant si cette instruction est une instance du psi-terme modélisant l'instruction cible. On obtient ainsi un procédé de recherche d'une instruction très efficace, en particulier adapté à la recherche d'une instruction dans un programme informatique comportant de nombreuses lignes de code informatique. Selon une première caractéristique avantageuse, l'étape de parcours comporte : - une étape de classification de l'instruction parcourue en fonction d'au moins un modèle d'instruction intermédiaire ; et en fonction du résultat de cette classification : -soit une étape d'arrêt du parcours ; -soit une étape de sélection d'au moins une prochaine instruction voisine de l'instruction parcourue dans le graphe, de façon à poursuivre le parcours du sous-graphe à partir de la prochaine instruction. Le procédé de recherche selon l'invention permet ainsi de limiter le parcours du graphe à un sous-graphe, en fonction de critères prédéfinis par l'utilisateur de ce procédé, ces critères étant examinés pour chaque n#ud parcouru. Le parcours du graphe s'effectue ainsi selon plusieurs sousgraphes, chaque sous-graphe ayant pour racine l'une des instructions sources. Selon une autre caractéristique particulièrement avantageuse, le procédé de recherche selon l'invention comporte une étape préalable au cours de laquelle on associe à chaque modèle d'instruction intermédiaire, une fonction booléenne s'appliquant à un identificateur d'une transition. Dans cette variante de réalisation, l'étape de sélection comporte le calcul du résultat de l'exécution de la fonction booléenne appliquée à l'identificateur de la transition entre l'instruction parcourue et la prochaine instruction. Ainsi, pour chaque n#ud parcouru associé à une instruction conforme au modèle d'une instruction intermédiaire, on décide quel sousgraphe de ce n#ud doit être parcouru, en exécutant la fonction booléenne appliquée aux transitions qui partent de ce n#ud. Cette caractéristique est particulièrement avantageuse car elle constitue un moyen de formalisation à la fois souple, puissant, et simple d'utilisation. Selon une autre caractéristique, l'instruction source est modélisée par au moins un modèle de type psi-terme. Cette caractéristique permet de rechercher facilement les racines des sous-graphes du graphe du flot de contrôle à parcourir pour rechercher l'instruction cible. Grâce à cette caractéristique, il n'est pas nécessaire de parcourir le graphe à partir du n#ud associé au point d'entrée du programme informatique. Selon une caractéristique particulièrement avantageuse, le procédé de recherche selon l'invention comporte une étape de lecture d'une mémoire comportant : -une première zone comportant un premier mot clef et au moins un modèle de l'instruction source ; -une deuxième zone comportant un deuxième mot clef et au moins un modèle de l'instruction cible ; et -une troisième zone comportant un troisième mot clef, et au moins un modèle de l'instruction intermédiaire et la fonction booléenne associée à ce modèle. Dans un mode préféré de réalisation, cette mémoire est constituée par un fichier informatique, dans lequel l'utilisateur mémorise les modèles d'instructions, le fichier comportant différentes sections repérées par les mots clefs pour séparer les instructions sources, les instructions intermédiaires et les instructions cibles. Ce mode préféré de réalisation est particulièrement souple d'utilisation. Selon un autre aspect, l'invention vise un procédé de détection d'une erreur de programmation dans un programme informatique, le procédé de détection mettant en #uvre un procédé de recherche tel que décrit succinctement ci-dessus, pour rechercher une séquence constituée d'une première, éventuellement d'au moins une deuxième, et d'une dernière instructions dans le programme, ces instructions s'exécutant successivement dans le programme, la première instruction étant l'instruction source précitée, la dernière instruction étant l'instruction cible précitée et l'éventuelle deuxième instruction étant une instruction intermédiaire précitée, l'erreur de programmation étant détectée en fonction du résultat de cette recherche. Selon un autre aspect, l'invention vise un système de génération de code informatique comportant : -un compilateur adapté à lire un programme informatique et à fournir un graphe comportant les transitions entre les instructions du programme informatique ; et -des moyens adaptés à mettre en #uvre un procédé de détection d'erreurs tel que décrit succinctement ci-dessus. Selon un autre aspect, l'invention vise un système informatique comportant des moyens adaptés à mettre en oeuvre un procédé de recherche tel que décrit succinctement ci-dessus. Les avantages et caractéristiques particulières propres au procédé de détection d'erreurs, au système de génération de code informatique et au système informatique étant les mêmes que ceux exposés ci-dessus concernant le procédé de recherche selon l'invention, ils ne seront pas rappelés ici. D'autres aspects et avantages de la présente invention apparaîtront plus clairement à la lecture de la description de modes particuliers de réalisation qui va suivre, cette description étant donnée uniquement à titre d'exemple non limitatif et faite en référence aux dessins annexés sur lesquels : -la figure 1 représente un graphe du flot de contrôle ; -la figure 2 représente un fichier de règles conforme à la présente invention ; -la figure 3 représente un sous-graphe du graphe de la figure 1 obtenu par un procédé de détection d'erreurs conforme à la présente invention ; -la figure 4 représente sous forme d'organigramme, les principales étapes d'un procédé de détection d'une erreur de programmation dans un programme informatique, dans un mode préféré de réalisation conforme à la présente invention ; et - la figure 5 représente schématiquement un système informatique comportant des moyens adaptés à mettre un oeuvre un procédé de recherche conforme à la présente invention, dans un mode préféré de réalisation. Par ailleurs la description est accompagnée des annexes suivantes : - annexe A : exemple détaillé d'un fichier de règles conforme à la présente invention; - annexes B et C : exemples de psi-termes ; annexe D : exemple d'une fonction booléenne associée à une instruction intermédiaire, conformément à la présente invention. La présente invention va maintenant être décrite, à titre d'exemple nullement limitatif, dans le contexte de la détection d'une erreur de programmation particulièrement fréquente, notamment dans le domaine de la programmation informatique dite "programmation système". Selon une règle R de programmation connue, il est fortement souhaitable de déverrouiller un verrou (en anglais "lock") préalablement verrouillé avant de quitter une fonction. Dans bien des cas, cette règle de programmation n'est pas respectée, ce qui entraîne des comportements inattendus du programme informatique lors de son exécution. La figure 1 est un exemple typique d'un graphe du flot de contrôle (CFG) (en anglais "Control Flow Graph") d'un programme informatique P ne respectant pas cette règle R de programmation. Le graphe CFG comporte un premier n#ud associé à une instruction 1100 de verrouillage d'un verrou 1 au moyen de l'instruction informatique lock(). L'instruction 1100 est suivie par une instruction de test 1110. Selon une première transition t1, l'instruction de test 1110 est suivie par une instruction 1120 de déverrouillage du verrou 1 au moyen de l'instruction informatique unlock(1). L'instruction 1120 est suivie par une instruction 1130 au cours de laquelle on quitte le programme P, en utilisant l'instruction informatique return. Ainsi, lorsque l'on suit cette transition t1, le verrou 1 est déverrouillé avant de quitter le programme informatique et la règle R est respectée. En revanche, lorsque l'on suit une deuxième transition t2 à partir de l'instruction de test 1110, on trouve une instruction 1140 associée à l'instruction return de fin du programme informatique P sans avoir préalablement déverrouillé le verrou 1. La séquence constituée par les instructions 1100, 1110 et 1140 ne respecte donc pas la règle R de programmation. La règle de programmation R peut être reformulée de façon plus simple par la formule F suivante : F : "Existe-t-il dans le graphe CFG, un chemin C conduisant à un n#ud "return" à partir d'un n#ud "lock", ce chemin n'empruntant pas de n#ud "unlock"?" Cette nouvelle formulation F de la règle R permet de ramener le problème de détection d'erreurs à un problème de recherche d'un chemin dans le graphe CFG. Plus précisément, rechercher si le programme P enfreint la règle R revient à rechercher un chemin C dans le graphe CFG, ce chemin comportant : - une instruction source de type "lock(X)", où X est une valeur quelconque, - une instruction cible de type "return", ce chemin n'empruntant pas d'instruction intermédiaire de type "unlock(X)". Une fois le problème posé de cette façon, un sous-problème à résoudre est celui de la recherche, dans le graphe CFG, des instructions informatiques conformes aux instructions source, cible et intermédiaire, à savoir les instructions de type "lock(X)", "unlock(X)" et "return", X étant une valeur quelconque. Afin de résoudre ce sous-problème, il convient tout d'abord de modéliser les instructions source, cible et intermédiaire, puis de vérifier si les instructions du graphe CFG sont conformes à ces modèles. Conformément à la présente invention, les psi-termes sont utilisés pour modéliser l'instruction source "lock(X)", l'instruction intermédiaire "unlock(X)" et l'instruction cible "return". Les psi-termes de ces instructions sous sont respectivement les psi-termes donnés aux annexes B, C et le psi-terme "return stmt". Dans le mode de réalisation décrit ici, on associe à chaque modèle d'instruction intermédiaire une fonction booléenne ayant comme paramètre d'entrée un identificateur d'une transition du graphe CFG, et dont le résultat d'exécution indique s'il est nécessaire ou non de poursuivre le parcours du graphe CFG en empruntant le n#ud qui suit le n#ud représentatif de cette instruction intermédiaire selon cette transition. Par exemple, conformément au problème F reformulé précédemment, si une instruction intermédiaire unlock(X) est trouvée dans un sous-graphe du graphe CFG ayant comme n#ud de départ l'instruction source lock(X), il n'est pas nécessaire de poursuivre le parcours du graphe CFG à partir des n#uds voisins de cette instruction intermédiaire, l'enchaînement des instructions lock(X) et unlock(X) étant conforme à la règle de programmation R. L'instruction intermédiaire unlock(X) est donc associée à la fonction booléenne "follow~none" dont le code est donné à l'annexe D, cette fonction renvoyant la valeur FALSE, quel que soit l'identificateur de la transition reçu en paramètre, pour signifier qu'il n'est pas nécessaire de poursuivre le parcours du sous-graphe à partir des voisins de l'instruction unlock(X). Nous allons maintenant décrire en référence à la figure 4 les principales étapes E400 à E470 d'un procédé de détection d'une erreur de programmation dans un programme informatique conformément à la présente invention. Ce procédé de détection d'une erreur de programmation recherche une séquence d'instructions composée d'une première instruction, d'une dernière instruction et éventuellement d'au moins une instruction intermédiaire, la première instruction, l'instruction intermédiaire et la dernière instruction s'exécutant successivement dans ce programme. Chacune de ces instructions est modélisée selon un modèle de type psi-terme tel que décrit précédemment. De même, chaque modèle d'instruction intermédiaire est associé à une fonction booléenne qui permet de décider dans quelle mesure il est nécessaire de poursuivre le parcours du sous-graphe à partir de cette instruction intermédiaire. Dans le mode de réalisation décrit ici, les modèles de ces instructions sont mémorisés dans une mémoire, par exemple un fichier informatique, suivant un format prédéterminé décrit maintenant en référence à la figure 2. La figure 2 représente un fichier de règles REG comportant : -une première zone comportant un premier mot clef "from" et au moins un modèle d'une instruction source ; -une deuxième zone comportant un deuxième mot clef "to" et au moins un modèle d'une instruction cible ; et, le cas échéant, -une troisième zone comportant un troisième mot clef "via" et au moins un modèle d'une instruction intermédiaire j et la fonction booléenne f, associée à ce modèle. Un exemple de fichier de règles REG permettant de détecter les erreurs de programmation violant la règle R est donné à l'annexe A. On notera, en référence à l'annexe A, que dans un mode de réalisation préféré de la présente invention, on peut également utiliser un mot clef "not", lorsque l'erreur de programmation à détecter est exprimée de façon négative, comme c'est le cas dans la formulation F. Bien entendu, le fichier de règles REG, peut contenir plusieurs instructions sources, plusieurs instructions cibles et plusieurs instructions intermédiaires. Par exemple, pour rechercher les erreurs de programmation associées à la règle R' suivante : "II est fortement souhaitable de "desallouer" une structure de données préalablement allouée avant de sortir d'une fonction qui utilise cette structure de manière temporaire", on peut reformuler cette règle de la façon suivante : "Existe-t-il dans le graphe CFG un chemin C conduisant à un n#ud "return" à partir d'un n#ud "malloc(X)", ce chemin n'empruntant pas de n#ud "free (X)" ?". Cette règle peut être décrite par un fichier de règles REG' contenant les psi-termes suivants : from malloc(X), to exit~node or retum~stmt, via free (X) -> follow~none or modify~expr(op~0=>X) => follow~none et contenant les définitions suivantes : function malloc(X) is call-expr( fn=>function decl(name=>identifier node(strg=>"malloc") ), args=>tree~list(value=>X)) function free (X) call-expr( fn=>function decl(name=>identifier node(strg=>"free") ), isargs=>tree~list(valu=>X))" Le fichier de règles REG est un paramètre d'entrée du procédé de détection dans le mode préféré de réalisation décrit en référence à la figure 4. Comme le montre la figure 4, au cours d'une première étape E400, on crée une liste "liste" vide. Cette étape E400 est suivie par une boucle constituée par les étapes E405, E410 et E415, au cours de laquelle on remplit la liste "liste" avec les n#uds du graphe CFG conformes au modèle d'instruction source lu dans le fichier de règles REG. Plus précisément, au cours de l'étape E405, on vérifie si tous les noeuds du graphe CFG ont été traités. Lorsque tel n'est pas le cas, on regarde si le n#ud en cours de traitement est conforme au modèle de l'instruction source. Dans l'exemple de la figure 1, on regarde donc si les instructions 1100 à 1130 (figure 1) sont conformes au modèle de l'instruction lock(X) donné à l'annexe B. En pratique, cela s'effectue en vérifiant si une instruction associée au n#ud "n#ud" du graphe CFG est une instance du modèle de l'instruction source. Si tel est le cas, le résultat du test E410 est positif. Ce test est alors suivi par une étape E415, au cours de laquelle on ajoute le n#ud "n#ud" testé au test E410 dans la liste "liste". En revanche, si le n#ud "n#ud" n'est pas conforme au modèle de l'instruction source, le résultat du test E410 est négatif. Ce test est alors suivi par l'étape E405 au cours de laquelle on recherche le n#ud "n#ud" suivant dans le graphe CFG. Lorsque tous les n#uds du graphe CFG ont été traités, l'étape E405 est suivie par une étape E420 au cours de laquelle on crée une liste vide "parcouru". L'étape E420 est suivie par une boucle constituée par les étapes E425 à E460. Au cours de l'étape E425, on regarde si la liste "liste" remplie au cours de la boucle constituée par les étapes E405 à E415 comporte au moins un élément. Lorsque tel n'est pas le cas, cette étape E425 est suivie par une étape E470 au cours de laquelle le procédé de détection selon l'invention se termine en retournant la valeur "FAUX". Cela signifie que la séquence d'instructions constituée par l'instruction source, l'instruction intermédiaire et l'instruction cible n'a pas été identifiée dans le graphe CFG. Tant que la liste "liste" est non vide, l'étape E425 est suivie par une étape E430, au cours de laquelle on extrait un n#ud "n#ud" de la liste "liste". L'étape E430 est suivie par un test E435 au cours duquel on vérifie si ce n#ud "n#ud" est un élément de la liste "parcouru" créée à l'étape E420. Si tel est le cas, le test E435 est suivi par l'étape E425 déjà décrite. Lorsque le n#ud 'n#ud" n'est pas compris dans la liste "parcouru", le résultat du test E435 est négatif. Ce test est alors suivi par une étape E440 au cours de laquelle on ajoute le n#ud "n#ud" dans la liste "parcouru". L'étape E440 est suivie par un test E445 au cours duquel on vérifie si le n#ud "n#ud" extrait à l'étape E430 est conforme au modèle de l'instruction cible du fichier de règles REG. Si tel est le cas, cela signifie que l'instruction cible a été identifiée dans un sous-graphe ayant pour racine un n#ud associé à une instruction conforme au modèle d'instruction source du fichier REG. Dans ce cas, le résultat du test E445 est positif. Ce test est alors suivi par une étape E450 au cours de laquelle le procédé de détection conforme à la présente invention se termine en retournant la valeur "VRAI". En revanche, lorsque le n#ud "n#ud" n'est pas conforme au modèle de l'instruction cible, le résultat du test E445 est négatif. Ce test est alors suivi par une boucle constituée par les étapes E451 à E465 s'exécutant pour tous les voisins "voisin" du n#ud "n#ud" dans le graphe CFG. Plus précisément, au cours de l'étape E451, on vérifie si tous les voisins du n#ud "n#ud" ont été traités. Si tel n'est pas le cas, l'étape E451 est suivie par un test E455 au cours duquel on vérifie si le n#ud "n#ud" est conforme à au moins un modèle d'instruction intermédiaire contenu dans le fichier de règles REG. Si le n#ud "n#ud" n'est conforme à aucun modèle d'instruction intermédiaire, le résultat du test E455 est positif. Ce test est alors suivi par une étape E460 au cours de laquelle on ajoute à la liste "liste", le voisin "voisin" du n#ud "n#ud". Dans ce mode de réalisation en effet, on décide par convention que si une instruction parcourue n'est conforme à aucun modèle du fichier de règles REG, on continue le parcours selon tous les sous-graphes de ce n#ud. En revanche, si le n#ud est conforme à au moins un modèle d'instruction intermédiaire j, le résultat du test E455 est négatif. Ce test est alors suivi par un test E465 au cours duquel on calcule le résultat de la fonction booléenne f, associée à la transition entre le n#ud "n#ud" et le voisin "voisin" de ce n#ud. Lorsque le résultat de cette fonction booléenne fj est positif, le test E465 est suivi par l'étape E460 déjà décrite, étape au cours de laquelle on ajoute le voisin "voisin" à la liste "liste". Si le résultat d'exécution de cette fonction booléenne f, est négatif, le test E465 est suivi par l'étape E451 déjà décrite. De même, l'étape E460 au cours de laquelle on ajoute le voisin "voisin" dans la liste "liste" est suivie par l'étape E451. Lorsque tous les voisins "voisin" du n#ud "n#ud" ont été traités, l'étape E451 est suivie par l'étape E425 déjà décrite. Ainsi, le procédé de détection conforme à la présente invention retourne la valeur "VRAI" dès qu'un élément de la liste "liste" est conforme au modèle cible et la valeur "FAUX" dans le cas contraire. La figure 3 représente un sous-graphe du graphe CFG obtenu par le procédé de détection d'erreurs décrit précédemment en référence à la figure 4. Conformément à la présente invention, à l'issue de la boucle constituée par les étapes E405 à E415, la liste "liste" contenait le n#ud 1100, seule instruction conforme à l'instruction source contenue dans la première zone des règles de l'annexe A. Puis, l'instruction 1110 a été ajoutée à la liste "liste" à la première exécution de l'étape E460, car l'instruction 1100 n'étant conforme à aucun modèle d'instruction intermédiaire, le résultat du test E455 était positif. De même, lorsque le n#ud "n#ud" a pris la valeur du n#ud associé à l'instruction 1110, l'instruction 1110 n'étant conforme à aucun modèle d'instruction intermédiaire, le résultat du test E455 était positif et les n#uds 1120 et 1140 ont été ajoutés à la liste "liste". En revanche, lorsque le n#ud "n#ud" a pris la valeur du n#ud associé à l'instruction 1120, l'instruction 1120 étant conforme au modèle de l'instruction intermédiaire "unlock(X)", le résultat du test E455 était négatif. Le résultat de la fonction follow~none associée à ce n#ud 1120, exécutée avec l'identifiant de transition t3 entre l'instruction 1120 et l'instruction 1130, a fourni un résultat négatif et le parcours du sous-graphe s'est arrêté pour cette branche, ce qui est symbolisé par l'absence de flèche entre les noeuds 1120 et 1130 sur la figure 3. Enfin, lorsque le n#ud "n#ud" a pris la valeur du n#ud associé à l'instruction 1140, l'instruction 1140 étant conforme au modèle cible, le résultat du test E445 était positif. Le procédé de détection selon l'invention a donc retourné la valeur "VRAI" à l'étape E450, cette valeur étant représentative de la présence de la séquence d'instructions "lock(X), return" recherchée, cette séquence d'instructions constituant une erreur de programmation enfreignant la règle de programmation R. En pratique, le procédé de détection selon l'invention peut être mis en #uvre dans un système de génération de code informatique comportant en particulier un compilateur adapté à fournir le graphe du flot de contrôle de ce programme. Selon un mode préféré de réalisation, le procédé de vérification peut être mis en #uvre par une extension de logiciel ("plug in" en anglais), chargée dans un compilateur extensible au moment de la compilation du programme informatique. Le compilateur gcc, à partir de la version 3. 0, peut constituer le point de départ d'un tel compilateur extensible. Dans ce mode de réalisation, le compilateur extensible génère le code exécutable à partir du code source du programme informatique de façon connue, mais en produisant, le cas échéant, des messages représentatifs de la détection d'une erreur de programmation, lorsqu'une erreur de programmation est détectée conformément aux règles de programmation spécifiées dans le fichier de règles REG. Le nom du fichier de règles REG peut être spécifié en paramètre d'une commande de compilation du programme informatique. Selon une variante, le procédé de vérification peut être intégré à un compilateur, auquel cas la détection d'erreurs de programmation s'effectue pendant la construction du graphe CFG. La figure 5 représente schématiquement un système informatique comportant des moyens adaptés à mettre un #uvre un procédé de recherche conforme à la présente invention, dans un mode préféré de réalisation. Ce système peut notamment être constitué par un ordinateur. Dans l'exemple de réalisation décrit ici, le système informatique comporte un clavier 510, un écran 509, reliés à un port d'entrées-sorties 503 d'une carte de traitement 501. La carte de traitement 501 comporte, reliés entre eux par un bus d'adresses et de données 502 : - une unité centrale de traitement 500 ; - une mémoire vive RAM 504 ; - une mémoire morte ROM 505 ; - une mémoire non volatile DISK 506 et - le port d'entrées-sorties 503. Chacun des éléments illustrés en figure 5 est bien connu de l'homme du métier des micro-ordinateurs et, plus généralement, des systèmes de traitement de l'information. Ces éléments communs ne sont donc pas décrits ici. La mémoire non volatile DISK 506, par exemple constituée par un disque dur, comporte notamment des registres pour mémoriser : - le code source du programme informatique P ; -le graphe CFG du flot de contrôle du programme P ; et-le fichier de règles REG. La mémoire vive 504 comporte notamment des registres "n#ud", "voisin", "liste" et "parcouru" pour mémoriser les variables de même nom décrites précédemment en référence à la figure 4. La mémoire morte 505 est adaptée à conserver le programme de fonctionnement de l'unité centrale de traitement 500. Elle comporte notamment un registre "Program" pour mémoriser les instructions d'un programme mettant en #uvre un procédé de recherche conforme à l'invention, tel que décrit précédemment en référence à l'organigramme de la figure 4. La mémoire morte 505 comporte également un registre "Compilateur" pour mémoriser un compilateur adapté à produire le graphe CFG à partir du code source du programme informatique P. ANNEXES ANNEXE A not from lock(X) to return stmt via unlock (X)-> follow~none ANNEXE B function lock(X) is call~expr( fn=>function-decl(name=>identifier~node(strg=>"lock") ), args=>tree~list(valu=>X)) ANNEXE C function unlock(X) is call~expr( fn=>function~decl(name->identifier~node(strg=>"unlock") ), args=>tree~list(value=>X)) ANNEXE D function follow~none(EdgeNo) is false REVENDICATIONS 1. Procédé de recherche d'au moins une instruction cible dans un programme informatique représenté sous forme d'un graphe (CFG) comportant des transitions entre des instructions dudit programme informatique, caractérisé en ce qu'il comporte : - une étape de modélisation de ladite instruction cible par au moins un modèle de type psi-terme ; -une étape de parcours d'un sous-graphe dudit graphe (CFG) à partir d'au moins une instruction source, en testant pour chaque instruction parcourue dans ledit sous-graphe, si ladite instruction parcourue est conforme au modèle de ladite instruction cible. 2. Procédé de recherche selon la revendication 1, caractérisé en ce que ladite étape de parcours comporte : - une étape de classification de ladite instruction parcourue en fonction d'au moins un modèle d'instruction intermédiaire ; eten fonction du résultat de ladite classification : -soit une étape d'arrêt du parcours ; -soit une étape de sélection d'au moins une prochaine instruction voisine de ladite instruction parcourue dans ledit graphe (CFG), de façon à poursuivre le parcours dudit sous-graphe à partir de ladite au moins une prochaine instruction. 3. Procédé de recherche selon la revendication 2, caractérisé en ce qu'il comporte : -une étape préalable au cours de laquelle on associe à chaque modèle d'instruction intermédiaire, une fonction booléenne s'appliquant à un identificateur d'une transition ; et en ce que - ladite étape de sélection comporte le calcul du résultat de l'exécution de ladite fonction booléenne appliquée à l'identificateur de la transition entre ladite instruction parcourue et ladite prochaine instruction. 4. Procédé de recherche selon l'une quelconque des revendications 1 à 3, caractérisé en ce que ladite au moins une instruction source est modélisée par au moins un modèle de type psi-terme. 5. Procédé de recherche selon la revendication 4, caractérisé en ce qu'il comporte une étape de lecture d'une mémoire comportant : -une première zone comportant un premier mot clef (from) et au moins un modèle de ladite au moins une instruction source ; -une deuxième zone comportant un deuxième mot clef (to) et au moins un modèle de ladite au moins une instruction cible ; et -une troisième zone comportant un troisième mot clef (via), et au moins un modèle de ladite au moins une instruction intermédiaire et ladite fonction booléenne associée à ce modèle. 6. Procédé de détection d'une erreur de programmation dans un programme informatique, caractérisé en ce qu'il met en oeuvre un procédé de recherche selon la revendication 1 pour rechercher une séquence constituée d'une première et d'une dernière instructions dans ledit programme, lesdites première et dernière instructions s'exécutant successivement dans ledit programme, la première instruction étant ladite instruction source et la dernière instruction étant ladite instruction cible, ladite erreur de programmation étant détectée en fonction du résultat de ladite recherche. 7. Procédé de détection d'une erreur de programmation dans un programme informatique, caractérisé en ce qu'il met en #uvre un procédé de recherche selon l'une quelconque des revendications 2 à 5 pour rechercher une séquence comportant une première, au moins une deuxième, et une dernière instructions dans ledit programme, lesdites première, au moins une deuxième, et dernière instructions s'exécutant successivement dans ledit programme, la première instruction étant ladite instruction source, ladite au moins une deuxième instruction étant une instruction intermédiaire, et la dernière instruction étant ladite instruction cible, ladite erreur de programmation étant détectée en fonction du résultat de ladite recherche. 8. Système de génération de code informatique comportant : -un compilateur adapté à lire un programme informatique et à fournir un graphe (CFG) comportant les transitions entre les instructions dudit programme informatique ; et -des moyens adaptés à mettre en #uvre un procédé de détection d'erreurs selon la revendication 6 ou 7. 9. Système informatique caractérisé en ce qu'il comporte des moyens adaptés à mettre en #uvre un procédé de recherche selon l'une quelconque des revendications 1 à 5.