cpachecker

Introdução ao Cpachecker

• Instruções de instalação
• Diretrizes de contribuição
• Instruções de desenvolvimento

Mais documentação pode ser encontrada no doc/ Diretório.

Licença e direitos autorais

O Cpachecker está licenciado sob a licença Apache 2.0 com direitos autorais de Dirk Beyer e outros (cf. Authors.md para obter uma lista completa de todos os colaboradores). As bibliotecas de terceiros estão sob várias outras licenças e direitos autorais, cf. Os arquivos nas LICENSES diretório para os textos completos da licença. Em particular, o Mathsat está disponível apenas para fins de pesquisa e avaliação (cf. LICENSES/LicenseRef-MathSAT-CPAchecker.txt ); portanto, use um solucionador SMT diferente, se necessário. Observe que, embora um programa GPL seja distribuído junto com o CPACHECKER, o CPACHECKER é separado desse programa e, portanto, não nos termos da GPL.

Prepare programas para verificação por cpachecker

Todos os programas precisam pré-processados ​​com o pré-processador C, ou seja, eles podem não conter diretivos #define e #include . Você pode ativar o pré-processamento dentro do cpachecker especificando --preprocess na linha de comando. Vários arquivos C podem ser fornecidos e serão vinculados e verificados como um único programa (recurso experimental).

Cpachecker é capaz de analisar e analisar um grande subconjunto de (GNU) c. Se a análise falhar para o seu programa, envie um relatório para [email protected].

Verificando um programa com cpachecker

1. Escolha um arquivo de código -fonte que você deseja ser verificado. Se você usar seu próprio programa, lembre-se de pré-processá-lo, como mencionado acima. Exemplo: doc/examples/example.c ou doc/examples/example_bug.c Uma boa fonte para mais programas de exemplos é o repositório de benchmarks SV que é, por exemplo, usado pela competição internacional em verificação de software.

2. Opcionalmente: se você deseja escolher determinadas análises como análise de predicado, especifique um arquivo de configuração. Este arquivo define, por exemplo, quais CPAs são usados. Os arquivos de configuração padrão podem ser encontrados na config/ . Se você não deseja uma análise específica, recomendamos a configuração padrão do cpachecker. No entanto, observe que, se você estiver no MacOS, você precisa fornecer binários Mathsat especificamente compilados para a configuração padrão para funcionar (ou usar o Docker para executar a versão Linux do cpachecker). A configuração do cpachecker é explicada em doc/Configuration.md .

3. Escolha um arquivo de especificação (você pode não precisar disso para algumas configurações). As configurações padrão usam config/specification/default.spc como especificação padrão. Com este, o CPACHECKER procurará etiquetas denominadas ERROR (insensíveis ao caso) e afirmações no arquivo de código -fonte. Outros exemplos para especificações podem ser encontrados na config/specification/ no diretório cpachecker.

4. Executar bin/cpachecker [ --config <CONFIG_FILE> ] [ --spec <SPEC_FILE> ] <SOURCE_FILE> Argumentos adicionais da linha de comando são descritos em doc/Configuration.md . Para usar a configuração padrão do cpachecker, passe apenas o arquivo de origem: bin/cpachecker doc/examples/example.c . Uma análise específica (como K-indução) pode ser escolhida, por exemplo, com bin/cpachecker --config/kInduction.properties doc/examples/example.c ou o equivalente a abreviatura bin/cpachecker --kInduction doc/examples/example.c . Java 17 ou posterior é necessário. Se não estiver no seu caminho, você precisará especificá -lo na variável de ambiente Java. Exemplo: export JAVA=/usr/lib/jvm/java-17-openjdk-amd64/bin/java para 64bit OpenJdk 17 no Ubuntu.

   Observe que nem todas as configurações de análise estão disponíveis para macOS porque não enviamos binários para solucionadores de SMT para esta plataforma. Você precisa construir os binários apropriados ou usar análises menos poderosas que trabalham com solucionadores baseados em Java, por exemplo, este em vez da configuração padrão do CPACHECKER: --predicateAnalysis-linear --option solver.solver=SMTInterpol é claro que você também pode usar soluções como o Docker para execução da versão Linux da versão do CPACK.

   Se você instalou o cpachecker usando o Docker, a linha de comando de exemplo acima ficaria assim: docker run -v $(pwd):/workdir -u $UID:$GID sosylab/cpachecker /cpachecker/doc/examples/example.c Cpachecker. Os arquivos de saída do cpachecker serão colocados em ./output/ .

5. Além da saída do console, um relatório HTML interativo é gerado na output/ , nomeado Report.html (para resultado true) ou Counterexample.*.html (para resultado false). Abra esses arquivos em um navegador para visualizar o resultado da análise do CPACHECKER (cf. doc/Report.md )

Também existem arquivos de saída adicionais na output/ :

• ARG.dot : Visualização da árvore de acessibilidade abstrata (formato graphviz)
• cfa*.dot : Visualização do Automaton de Fluxo de Controle (Formato GraphViz)
• reached.dot : Visualização do Automaton de Fluxo de Controle com os estados abstratos visualizados no topo (Formato GraphViz)
• coverage.info : informações de cobertura (semelhantes às das ferramentas de teste) no formato Gcov Use a seguinte linha de comando para gerar um relatório HTML como output/index.html : genhtml output/coverage.info --output-directory output --legend
• Counterexample.*.txt : um caminho através do programa que leva a um erro
• Counterexample.*.assignment.txt : atribuições para todas as variáveis ​​no caminho do erro.
• Counterexample.*.harness.c Consulte Doc/Tutoriais/Test-Harness.md para um exemplo de uso.
• predmap.txt : predicados usados ​​por análise de predicado para provar a segurança do programa
• reached.txt : despejo de todos os estados abstratos alcançados
• Statistics.txt : Estatísticas de tempo (também podem ser impressas para consolar com --stats )

Observe que nem todos esses arquivos estarão disponíveis para todas as configurações. Além disso, alguns desses arquivos são produzidos apenas se um erro for encontrado (ou vice-versa). Cpachecker substituirá os arquivos neste diretório!

Validando um programa com cpa-witness2test

Você pode validar testemunhas de violação com o CPA-Witness2test, que faz parte do Cpachecker.

1. Para fazer isso, você precisa de uma testemunha de violação, um arquivo de especificação que se encaixa na testemunha de violação e o arquivo de código -fonte que se encaixa na testemunha de violação.

2. Para validar a testemunha, execute o seguinte comando:

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

   Os argumentos da linha de comando addcional são visualizados com bin/cpa-witness2test -h .

3. Quando concluído, e se a testemunha de violação for validada com sucesso, a saída do console mostra Verification result: FALSE . Além da saída do console, o CPA-witness2test também cria uma output/*.harness.c . Esse arquivo pode ser compilado no arquivo de origem para criar um teste executável que reflita a testemunha de violação.

Observe que, se a testemunha de violação não contiver informações suficientes para criar um teste executável, o resultado da validação será ERROR e a saída do console conterá a seguinte linha: Could not export a test harness, some test-vector values are missing.