goto-cc - Online na nuvem

PROGRAMA:

NOME

cbmc - Verificador de modelo limitado para programas C / C ++ e Java

SINOPSE

cbmc [--propriedade id da propriedade] arquivo.c ...

cbmc [- propriedades do show] arquivo.c ...

cbmc [--todas as propriedades] arquivo.c ...

ir para-cc [-EU incluir caminho] [-c] arquivo.c [-ou arquivo de saída.o]

ir para instrumento no arquivo arquivo de saída

Apenas as opções mais úteis são listadas aqui; veja abaixo para o restante.

DESCRIÇÃO

cbmc gera traços que demonstram como uma afirmação pode ser violada, ou prova que
a asserção não pode ser violada dentro de um determinado número de iterações de loop. CBMC pode ler
código-fonte diretamente ou um goto-binário gerado por goto-cc. Os programas Java são fornecidos como
arquivos de classe. Sem quaisquer outras opções, cbmc verifica todas as propriedades (automaticamente
gerado ou especificado pelo usuário) encontrado no programa. Se alguma das propriedades pode ser
violada, um contra-exemplo é impresso e a análise é abortada. A análise pode ser
restrito a uma propriedade particular com a opção --property. O resultado da verificação
para todas as propriedades pode ser obtido por meio da opção --all-properties.

ir para-cc lê o código-fonte e gera um goto-binário. Sua interface de linha de comando é
projetado para imitar o de gcc(1). Observe em particular que ir para-cc distingue entre
fases de compilação e vinculação, assim como o gcc faz. cbmc espera um goto-binário para o qual
a ligação foi concluída.

ir para instrumento lê um goto-binário, executa uma determinada transformação de programa e, em seguida,
grava o programa resultante como goto-binário no disco.

O fluxo normal é (1) traduzir a fonte em um goto-binário usando goto-cc, então (2)
realizar a instrumentação com goto-instrument, e finalmente (3) realizar a análise com
cbmc.

OPÇÕES

FRONTEND OPÇÕES (cbmc e ir para-cc)
-Eu caminho
Definir caminho de inclusão (C / C ++)

-D macro
Definir macro de pré-processador (C / C ++)

--processo
Pare após o pré-processamento

--show-tabela de símbolos
Mostrar tabela de símbolos

--show-goto-funções
Mostrar programa goto

ARQUITETURAL OPÇÕES (cbmc e ir para-cc)
cbmc por padrão usa configurações arquitetônicas que correspondem às da máquina cbmc is
executado em, ou seja, as configurações abaixo são necessárias apenas ao verificar o software que está
destina-se a ser executado em uma arquitetura ou sistema operacional diferente. ir para-cc gera um goto-binário para um
arquitetura particular, ou seja, a arquitetura não pode ser alterada após o goto-binário ser
gerado.

--16, --32, --64
Definir a largura do int

--LP64, --ILP64, --LLP64, --ILP32, --LP32
Defina a largura de int, long e ponteiros

--pequeno endian
Permitir conversões de palavra-byte little-endian

--big-endian
Permitir conversões palavra-byte big-endian

--caracter não identifcado
Tornar "char" sem sinal por padrão

--arch Definir arquitetura de destino

--os Definir sistema operacional de destino

--sem arco
Não configure uma arquitetura

--sem biblioteca
Desativar biblioteca C abstrata integrada

--round-to-mais próximo, --round-to-plus-inf, --round-to-menos-inf, --round-to-zero
Modo de arredondamento de ponto flutuante IEEE para usar quando o programa começa (o padrão é redondo
para o mais próximo). O programa em verificação pode substituir esta configuração, por exemplo, com
cenário(3).

PROGRAMA INSTRUMENTAÇÃO OPÇÕES (cbmc e goto-instrumento)
Ambos cbmc e ir para instrumento pode gerar afirmações que detectam erros comuns específicos,
conforme listado abaixo.

--limites-check
Ativar verificações de limites de array

--div-por-zero-verificação
Habilitar divisão por verificações de zero

--pointer-check
Habilitar verificações de ponteiro

--signed-overflow-check
Habilita verificações aritméticas de over- e underflow para aritmética de inteiros assinados

--unsigned-overflow-check
Habilita verificações aritméticas de over- e underflow para aritmética de inteiros não assinados

--nan-verificar
Verifique os cálculos de ponto flutuante para NaN

--sem asserções
Ignorar asserções fornecidas pelo usuário

- sem suposições
Ignorar suposições fornecidas pelo usuário

- rótulo de rótulo de erro
Verifique se o rótulo fornecido está inacessível

PROGRAMA INSTRUMENTAÇÃO OPÇÕES (ir para instrumento apenas)
ir para instrumento suporta transformações de programa mais complexas.

--não-volátil
Faz leituras de variáveis ​​voláteis não determinísticas

- função isr
Instrumenta uma rotina de serviço de interrupção com o nome fornecido

- E / S mapeada pela memória da mmio Instruments

--nondet-estático
Variáveis ​​com vida útil estática são inicializadas de forma não determinística

--dump-c
Código-fonte ANSI-C de saída em vez de um binário goto.

BMC OPÇÕES (cbmc)
--todas as propriedades
Relatório de status de todas as propriedades

--show-propriedades
Mostrar apenas propriedades

--show-loops
Mostra os loops no programa

--cover-afirmações
Verifique quais afirmações são acessíveis

--nome da função
Definir o nome da função principal

- id da propriedade
Verifique apenas a propriedade específica com o identificador fornecido

- somente programa
Mostra apenas a expressão do programa

--profundidade nº
Limite a profundidade da pesquisa

--descontrair nr
Unwind loops nr vezes

--unwindset L: B, ...
Desenrole o loop L com um limite de B (use --show-loops para obter os IDs do loop)

--show-vcc
Mostrar as condições de verificação

--fórmula de fatia
Remover atribuições não relacionadas à propriedade

--não-desenrolamento-asserções
Não gere afirmações desdobráveis

--nomes-bonitos
Não simplifique os identificadores

PROCESSO INTERNO OPÇÕES (cbmc)
--dimacs
Gerar CNF no formato DIMACS para uso por solucionadores SAT externos

- embelezar-ganancioso
Embeleze o contra-exemplo (heurística gananciosa)

--smt1 Subobjetivos de saída na sintaxe SMT1 (experimental)

--smt2 Subobjetivos de saída na sintaxe SMT2 (experimental)

--boolector
Usar Boolector (experimental)

--mathsat
Usar MathSAT (experimental)

--cvc Usa CVC3 (experimental)

- sim
Use Yices (experimental)

--z3 Usar Z3 (experimental)

--refinar
Use o procedimento de refinamento (experimental)

--outfile nome do arquivo
Fórmula de saída para determinado arquivo

--arrays-uf-nunca
Nunca transforme matrizes em funções não interpretadas

--arrays-uf-sempre
Sempre transforme matrizes em funções não interpretadas

MEIO AMBIENTE

Todas as ferramentas respeitam a variável de ambiente TMPDIR ao gerar arquivos temporários e
diretórios. Além disso, observe que o pré-processador usado pelo CBMC usará o ambiente
variáveis ​​para localizar arquivos de cabeçalho. GOTO-CC visa aceitar todas as variáveis ​​de ambiente que
GCC faz.

DIREITOS AUTORAIS

2001-2014, Daniel Kroening, Edmund Clarke

Use goto-cc online usando serviços onworks.net