klee uclibc

KLEE-uClibc

Il s'agit d'une version modifiée d'uClibc pour KLEE. Veuillez consulter le fichier README pour plus d'informations sur uClibc.

Pour créer uClibc pour KLEE :

1. Assurez-vous llvm-config est dans votre PATH (ou défini en utilisant --with-llvm-config ). La version LLVM utilisée par llvm-config doit correspondre à la version LLVM utilisée par le compilateur C LLVM Bitcode que vous avez l'intention d'utiliser à l'étape 2.

2. Assurez-vous d'avoir l'un des compilateurs C LLVM suivants

• clang construit dans le répertoire de l'outil LLVM ( llvm-config --bindir )
• clang dans votre PATH

Le compilateur C à utiliser sera recherché dans l'ordre ci-dessus avec le premier compilateur fonctionnel à utiliser.

Notez que vous pouvez également forcer un compilateur C particulier en utilisant la variable d'environnement CC ou en utilisant --with-cc avec le script de configuration.

3. Exécutez le script de configuration.

   $ ./configure --make-llvm-lib

   Pour voir toutes les options exécutées

   $ ./configure --help

4. Par défaut, un fichier .config pré-construit par uClibc sera ajouté au répertoire racine d'uClibc par le script de configuration. Ceci est fait pour faciliter la compilation pour les utilisateurs. Cependant, l'indicateur --disable-prebuilt-config peut être utilisé pour empêcher l'ajout d'un fichier .config . Si vous souhaitez créer votre propre .config vous pouvez le faire en exécutant make menuconfig ou make config après avoir exécuté le script configure.

5. Compiler

   $ make

   Vous pouvez également ajouter des indicateurs facultatifs en ajoutant KLEE_CFLAGS=... à la fin de la ligne make ci-dessus. En particulier, pour compiler printf, qui est exclu par défaut, utilisez :

   make KLEE_CFLAGS="-DKLEE_SYM_PRINTF"

   Pour compiler en mode optimisé, utilisez l'indicateur --enable-release . Attention, les choses pourraient se casser si vous faites cela.