goto-cc - Online nel cloud

PROGRAMMA:

NOME

cbmc - Bounded Model Checker per programmi C/C++ e Java

SINOSSI

CBMC [--proprietà ID-proprietà] file.c ...

CBMC [--mostra-proprietà] file.c ...

CBMC [--tutte le proprietà] file.c ...

vai-cc [-IO include-percorso] [-C] file.c [-O outfile.o]

goto-strumento infilare file di uscita

Qui sono elencate solo le opzioni più utili; vedi sotto per il resto.

DESCRIZIONE

CBMC genera tracce che dimostrano come un'asserzione può essere violata, o dimostra che
l'asserzione non può essere violata entro un dato numero di iterazioni del ciclo. CBMC può leggere
codice sorgente direttamente o un binario goto generato da goto-cc. I programmi Java sono dati come
file di classe. Senza ulteriori opzioni, cbmc controlla tutte le proprietà (automaticamente
generato o specificato dall'utente) trovato nel programma. Se una qualsiasi delle proprietà può essere
violato, viene stampato un controesempio e l'analisi viene interrotta. L'analisi può essere
limitato a una particolare proprietà con l'opzione --property. Il risultato della verifica
per tutte le proprietà può essere ottenuto mediante l'opzione --all-properties.

vai-cc legge il codice sorgente e genera un binario goto. La sua interfaccia a riga di comando è
progettato per imitare quello di gcc(1). Nota in particolare che vai-cc distingue tra
fasi di compilazione e collegamento, proprio come fa gcc. CBMC si aspetta un goto-binary per il quale
il collegamento è stato completato.

goto-strumento legge un binario goto, esegue una determinata trasformazione del programma e quindi
scrive il programma risultante come goto-binary su disco.

Il flusso usuale è (1) tradurre source in un goto-binary usando goto-cc, quindi (2)
eseguire la strumentazione con goto-instrument e infine (3) eseguire l'analisi con
CBMC.

VERSIONI

FRONTEND VERSIONI (CBM ed vai-cc)
-io percorso
Imposta percorso di inclusione (C/C++)

MrGreen macro
Definire la macro del preprocessore (C/C++)

--preprocesso
Interrompi dopo la preelaborazione

--mostra-tabella-simbolo
Mostra tabella dei simboli

--show-goto-funzioni
Mostra vai al programma

ARCHITETTONICO VERSIONI (CBM ed vai-cc)
CBMC per impostazione predefinita utilizza impostazioni architetturali che corrispondono a quelle della macchina CBMC is
eseguito su, ad esempio, le impostazioni di seguito sono necessarie solo quando si verifica il software che è
pensato per essere eseguito su un'architettura o un sistema operativo diversi. vai-cc genera un goto-binary per a
architettura particolare, cioè, l'architettura non può essere modificata dopo che il goto-binary è
generato.

--16, --32, --64
Imposta larghezza di int

--LP64, --ILP64, --LLP64, --ILP32, --LP32
Imposta la larghezza di int, long e puntatori

--Little Endian
Consenti conversioni word-byte little-endian

--big endian
Consenti conversioni big-endian word-byte

--carattere-senza segno
Rendi "char" non firmato per impostazione predefinita

--arch Imposta l'architettura di destinazione

--os Imposta il sistema operativo di destinazione

--no-arco
Non creare un'architettura

--no-libreria
Disabilita la libreria C astratta incorporata

--arrotondare al più vicino, --arrotondare a più inf, --arrotondare a meno inf, --arrotondare a zero
Modalità di arrotondamento in virgola mobile IEEE da utilizzare all'inizio del programma (l'impostazione predefinita è round
al più vicino). Il programma in fase di verifica può ignorare questa impostazione, ad es. con
feseround(3).

PROGRAMMA STRUMENTAZIONE VERSIONI (CBM ed goto-strumento)
Entrambi CBMC ed goto-strumento può generare asserzioni che catturano errori comuni specifici,
come di seguito elencati.

--controllo-limiti
Abilita i controlli dei limiti dell'array

--div-by-zero-controllo
Abilita divisione per zero controlli

--controllo-puntatore
Abilita i controlli del puntatore

--signed-overflow-check
Abilita i controlli aritmetici di overflow e underflow per l'aritmetica di interi con segno

--unsigned-overflow-check
Abilita i controlli aritmetici di overflow e underflow per l'aritmetica di interi senza segno

--nan-controlla
Controlla i calcoli in virgola mobile per NaN

--no-asserzioni
Ignora le asserzioni fornite dall'utente

--no-presunzioni
Ignora le ipotesi fornite dall'utente

--etichetta etichetta di errore
Verificare che l'etichetta data sia irraggiungibile

PROGRAMMA STRUMENTAZIONE VERSIONI (goto-strumento solo)
goto-strumento supporta ulteriori e più complesse trasformazioni del programma.

--non-volatile
Rende le letture da variabili volatili non deterministiche

--isr funzione
Strumenti una routine di servizio di interruzione con il nome dato

--mmio Instruments I/O mappati in memoria

--nondet-statico
Le variabili con durata statica vengono inizializzate in modo non deterministico

--dump-c
Emetti il ​​codice sorgente ANSI-C invece di un binario goto.

BMC VERSIONI (CBM)
--all-proprietà
Segnala lo stato di tutte le proprietà

--show-proprietà
Mostra solo proprietà

--show-loop
Mostra i loop nel programma

--cover-asserzioni
Controlla quali asserzioni sono raggiungibili

--nome funzione
Imposta il nome della funzione principale

--ID proprietà
Controlla solo la proprietà specifica con l'identificatore dato

--solo programma
Mostra solo l'espressione del programma

--profondità nr
Limita la profondità di ricerca

--rilassarsi nr
Svolgi loop nr volte

--srotolare L:B,...
Svolgi il ciclo L con un limite di B (usa --show-loops per ottenere gli ID del ciclo)

--mostra-vcc
Mostra le condizioni di verifica

--formula-fetta
Rimuovere le assegnazioni non correlate alla proprietà

--no-svolgimento-asserzioni
Non generare affermazioni snervanti

--senza-nomi-carini
Non semplificare gli identificatori

BACKEND VERSIONI (CBM)
--dimacs
Genera CNF in formato DIMACS per l'utilizzo da parte di risolutori SAT esterni

--beautify-avido
Abbellisci il controesempio (euristica avida)

--smt1 Output sottoobiettivi nella sintassi SMT1 (sperimentale)

--smt2 Output sottoobiettivi nella sintassi SMT2 (sperimentale)

--boolector
Usa Boolector (sperimentale)

--matematica
Usa MathSAT (sperimentale)

--cvc Usa CVC3 (sperimentale)

--sì
Usa Yices (sperimentale)

--z3 Usa Z3 (sperimentale)

--perfeziona
Usa procedura di perfezionamento (sperimentale)

--outfile nomefile
Formula di output nel file specificato

--arrays-uf-mai
Non trasformare mai gli array in funzioni non interpretate

--arrays-uf-sempre
Trasforma sempre gli array in funzioni non interpretate

AMBIENTE

Tutti gli strumenti rispettano la variabile di ambiente TMPDIR durante la generazione di file temporanei e
directory. Si noti inoltre che il preprocessore utilizzato da CBMC utilizzerà l'ambiente
variabili per individuare i file di intestazione. GOTO-CC mira ad accettare tutte le variabili d'ambiente che
GCC lo fa.

COPYRIGHT

2001-2014, Daniel Kroening, Edmund Clarke

Usa goto-cc online utilizzando i servizi onworks.net