cpachecker

Commencer avec Cpachecker

• Instructions d'installation
• Lignes directrices de contribution
• Instructions de développement

Plus de documentation peut être trouvée dans le répertoire doc/ .

Licence et droit d'auteur

CPachecker est concédé sous licence Apache 2.0 avec Copyright par Dirk Beyer et autres (cf. auteurs.md pour la liste complète de tous les contributeurs). Les bibliothèques tierces relèvent de diverses autres licences et droits d'auteur, cf. Les fichiers des LICENSES de répertoire pour les textes de licence complets. En particulier, MathSat est disponible à des fins de recherche et d'évaluation uniquement (cf. LICENSES/LicenseRef-MathSAT-CPAchecker.txt ), alors assurez-vous d'utiliser un autre solveur SMT différent si nécessaire. Notez que bien qu'un programme GPL soit distribué avec CPachecker, CPachecker est distinct de ce programme et donc pas sous les termes du GPL.

Préparer des programmes de vérification par CPachecker

Tous les programmes doivent être traités avec le pré-processeur C, c'est-à-dire qu'ils peuvent ne pas contenir de directives #define et #include . Vous pouvez activer le prétraitement à l'intérieur de CPachecker en spécifiant --preprocess à la ligne de commande. Plusieurs fichiers C peuvent être donnés et seront liés ensemble et vérifiés comme un seul programme (fonctionnalité expérimentale).

Cpachecker est capable d'analyser et d'analyser un grand sous-ensemble de (GNU) c. Si l'analyse échoue pour votre programme, veuillez envoyer un rapport à [email protected].

Vérification d'un programme avec CPachecker

1. Choisissez un fichier de code source que vous souhaitez vérifier. Si vous utilisez votre propre programme, n'oubliez pas de le prétraiter comme mentionné ci-dessus. Exemple: doc/examples/example.c ou doc/examples/example_bug.c Une bonne source pour plus d'exemples de programmes est le référentiel SV-Benchmarks qui est par exemple utilisé par la concurrence internationale sur la vérification des logiciels.

2. En option: si vous souhaitez choisir certaines analyses comme l'analyse du prédicat, spécifiez un fichier de configuration. Ce fichier définit par exemple les CPA utilisés. Les fichiers de configuration standard peuvent être trouvés dans le répertoire config/ . Si vous ne voulez pas d'analyse spécifique, nous recommandons la configuration par défaut de CPachecker. Cependant, notez que si vous êtes sur macOS, vous devez fournir des binaires MathSat spécialement compilés pour que la configuration par défaut fonctionne (ou utilisez Docker afin d'exécuter la version Linux de CPachecker). La configuration de CPachecker est expliquée dans doc/Configuration.md .

3. Choisissez un fichier de spécification (vous n'en avez peut-être pas besoin pour certaines configurations). Les configurations standard utilisent config/specification/default.spc comme spécification par défaut. Avec celui-ci, CPachecker recherchera des étiquettes nommées ERROR (cas insensible) et affirmations dans le fichier de code source. D'autres exemples de spécifications peuvent être trouvés dans config/specification/ dans le répertoire CPachecker.

4. Exécuter bin/cpachecker [ --config <CONFIG_FILE> ] [ --spec <SPEC_FILE> ] <SOURCE_FILE> Les arguments de ligne de commande supplémentaires sont décrits dans doc/Configuration.md . Pour utiliser la configuration par défaut de CPachecker, passez uniquement le fichier source: bin/cpachecker doc/examples/example.c . Une analyse spécifique (comme K-Induction) peut être choisie par exemple avec bin/cpachecker --config/kInduction.properties doc/examples/example.c ou l'abréviation équivalente bin/cpachecker --kInduction doc/examples/example.c . Java 17 ou version ultérieure est nécessaire. Si ce n'est pas sur votre chemin, vous devez le spécifier dans la variable d'environnement Java. Exemple: export JAVA=/usr/lib/jvm/java-17-openjdk-amd64/bin/java pour 64bit openjdk 17 sur ubuntu.

   Veuillez noter que toutes les configurations d'analyse ne sont pas disponibles pour MacOS car nous n'envoyons pas de binaires pour les solveurs SMT pour cette plate-forme. Vous devez soit créer vous-même les binaires appropriés, soit utiliser des analyses moins puissantes qui fonctionnent avec des solveurs basés sur Java, par exemple celui-ci au lieu de la configuration par défaut de Cpachecker: --predicateAnalysis-linear --option solver.solver=SMTInterpol bien sûr que vous pouvez également utiliser des solutions comme Docker pour exécuter la version linux de Cpachecker.

   Si vous avez installé Cpachecker à l'aide de Docker, la ligne de commande d'exemple ci-dessus ressemblerait à ceci: docker run -v $(pwd):/workdir -u $UID:$GID sosylab/cpachecker /cpachecker/doc/examples/example.c Cette commande rend le répertoire actuel disponible dans le conteneur, afin de vérifier un programme dans le répertoire actuel simplement fournir son nom de fichier à l'emploi. CPachecker. Les fichiers de sortie de cpachecker seront placés dans ./output/ .

5. De plus, à la sortie de la console, un rapport HTML interactif est généré dans la output/ , soit nommé Report.html (pour le résultat vrai) ou Counterexample.*.html (pour le résultat false). Ouvrez ces fichiers dans un navigateur pour afficher le résultat de l'analyse CPachecker (cf. doc/Report.md )

Il existe également des fichiers de sortie supplémentaires dans la output/ :

• ARG.dot : visualisation de l'arborescence abstraite d'accession (format Graphviz)
• cfa*.dot : Visualisation de Control Flow Automaton (Format Graphviz)
• reached.dot : visualisation de l'automate de flux de contrôle avec les états abstraits visualisés en haut (format Graphviz)
• coverage.info : informations de couverture (similaires à celles des outils de test) au format Gcov Utilisez la ligne de commande suivante pour générer un rapport HTML en tant que output/index.html : genhtml output/coverage.info --output-directory output --legend
• Counterexample.*.txt : un chemin à travers le programme qui mène à une erreur
• Counterexample.*.assignment.txt : affectations pour toutes les variables sur le chemin d'erreur.
• Counterexample.*.harness.c : un harnais de test qui peut reproduire le chemin d'erreur par l'exécution du test. Voir doc / tutoriels / test-stariness.md pour un exemple.
• predmap.txt : prédicats utilisés par l'analyse des prédicats pour prouver la sécurité du programme
• reached.txt : lemp de tous les états abstraits atteints
• Statistics.txt : statistiques de temps (peut également être imprimée pour consoler avec --stats )

Notez que tous ces fichiers ne seront pas disponibles pour toutes les configurations. Certains de ces fichiers ne sont également produits que si une erreur est trouvée (ou vice-versa). CPachecker écrasera les fichiers dans ce répertoire!

Valider un programme avec CPA-Witness2test

Vous pouvez valider des témoins de violation avec CPA-Witness2test, qui fait partie de CPachecker.

1. Pour ce faire, vous avez besoin d'un témoin de violation, d'un dossier de spécification qui correspond au témoin de violation et au dossier de code source qui correspond au témoin de violation.

2. Pour valider le témoin, exécutez la commande suivante:

    bin/cpa-witness2test --witness <WITNESS_FILE> --spec <SPEC_FILE> <SOURCE_FILE>`
   

   Les arguments de ligne de commande supplémentaires sont affichés avec bin/cpa-witness2test -h .

3. Une fois terminé, et si le témoin de violation est validé avec succès, la sortie de la console montre Verification result: FALSE . De plus, à la sortie de la console, CPA-Witness2Test crée également une output/*.harness.c . Ce fichier peut être compilé avec le fichier source pour créer un test exécutable qui reflète le témoin de violation.

Notez que si le témoin de violation ne contient pas suffisamment d'informations pour créer un test exécutable, le résultat de validation sera ERROR et la sortie de la console contiendra la ligne suivante: Could not export a test harness, some test-vector values are missing.