goto-cc - Online în cloud

PROGRAM:

NUME

cbmc - Bounded Model Checker pentru programe C/C++ și Java

REZUMAT

cbmc [--proprietate ID-ul proprietății] dosar.c ...

cbmc [--show-properties] dosar.c ...

cbmc [--toate-proprietăți] dosar.c ...

du-te-cc [-I include-cale] [-c] dosar.c [-sau outfile.o]

goto-instrument infile outfile

Aici sunt enumerate doar cele mai utile opțiuni; vezi mai jos pentru restul.

DESCRIERE

cbmc generează urme care demonstrează modul în care o afirmație poate fi încălcată sau dovedește acest lucru
afirmația nu poate fi încălcată într-un anumit număr de iterații în buclă. CBMC poate citi
codul sursă direct sau un binar goto generat de goto-cc. Programele Java sunt date ca
fișiere de clasă. Fără alte opțiuni, cbmc verifică toate proprietățile (automat
generate sau specificate de utilizator) găsite în program. Dacă oricare dintre proprietăți poate fi
încălcat, este tipărit un contraexemplu și analiza este întreruptă. Analiza poate fi
limitat la o anumită proprietate cu opțiunea --property. Rezultatul verificării
pentru toate proprietățile pot fi obținute prin intermediul opțiunii --all-properties.

du-te-cc citește codul sursă și generează un goto-binar. Interfața sa de linie de comandă este
conceput pentru a imita pe cel al gcc(1). Rețineți în special că du-te-cc distinge între
compilarea și legarea fazelor, la fel cum face gcc. cbmc așteaptă un goto-binar pentru care
legătura a fost finalizată.

goto-instrument citește un goto-binar, efectuează o transformare de program dată și apoi
scrie programul rezultat ca goto-binar pe disc.

Fluxul obișnuit este de a (1) traduce sursa într-un goto-binar folosind goto-cc, apoi (2)
efectuați instrumentarea cu goto-instrument și, în final (3) efectuați analiza cu
cbmc.

OPŢIUNI

ÎN FAȚĂ OPŢIUNI (cbmc și du-te-cc)
-I calea
Setați calea include (C/C++)

-D macro
Definiți macrocomanda preprocesorului (C/C++)

--preproces
Opriți după preprocesare

--arata-simbol-tabel
Afișați tabelul cu simboluri

--show-goto-functions
Afișați programul de acces

ARHITECTURAL OPŢIUNI (cbmc și du-te-cc)
cbmc în mod implicit utilizează setări arhitecturale care se potrivesc cu cele ale mașinii cbmc is
executat pe, adică setările de mai jos sunt necesare numai atunci când se verifică software-ul care este
menit să ruleze pe o arhitectură sau un sistem de operare diferit. du-te-cc generează un goto-binar pentru a
arhitectura particulară, adică, arhitectura nu poate fi schimbată după ce este binarul goto
generat.

--16, --32, --64
Setați lățimea pentru int

--LP64, --ILP64, --LLP64, --ILP32, --LP32
Setați lățimea int, long și pointers

--little-endian
Permite conversiile little-endian word-byte

--big-endian
Permite conversii big-endian cuvânt-octet

--unsigned-char
Faceți „char” nesemnat în mod prestabilit

--arch Setați arhitectura țintă

--os Setați sistemul de operare țintă

--fără-arc
Nu crea o arhitectură

--fără-bibliotecă
Dezactivați biblioteca C abstractă încorporată

--round-to-nearest, --round-to-plus-inf, --round-to-minus-inf, --round-to-zero
Modul de rotunjire în virgulă mobilă IEEE de utilizat când începe programul (implicit este rotund
cel mai apropiat). Programul în curs de verificare poate suprascrie această setare, de exemplu, cu
fesetround(3).

PROGRAMUL INSTRUMENTAŢIE OPŢIUNI (cbmc și du-te la instrument)
Ambele cbmc și goto-instrument poate genera afirmații care surprind anumite erori comune,
așa cum sunt enumerate mai jos.

--verificarea limitelor
Activați verificările limitelor matricei

--div-by-zero-check
Activați controalele de împărțire la zero

--pointer-check
Activați verificările indicatorului

--signed-overflow-check
Activați verificările aritmetice de depășire și depășire pentru aritmetica cu numere întregi cu semn

--unsigned-overflow-check
Activați verificările aritmetice de depășire și depășire pentru aritmetica cu numere întregi fără semn

--nan-check
Verificați calculele în virgulă mobilă pentru NaN

--fara-afirmatii
Ignorați afirmațiile furnizate de utilizator

--fără-presupune
Ignorați ipotezele furnizate de utilizator

--error-label etichetă
Verificați dacă eticheta dată nu este accesibilă

PROGRAMUL INSTRUMENTAŢIE OPŢIUNI (goto-instrument numai)
goto-instrument sprijină transformări de program ulterioare, mai complexe.

--nondet-volatil
Face citirile din variabilele volatile nedeterministe

--funcția isr
Instrumentează o rutină de serviciu de întrerupere cu numele dat

--mmio Instruments I/O mapat cu memorie

--nondet-static
Variabilele cu durata de viață statică sunt inițializate nedeterminist

--halda-c
Ieșiți codul sursă ANSI-C în loc de un binar goto.

BMC OPŢIUNI (cbmc)
--toate-proprietățile
Raportați starea tuturor proprietăților

--arata-proprietati
Afișați numai proprietăți

--arata-bucle
Afișați buclele din program

--aserțiuni-copertă
Verificați ce afirmații sunt accesibile

--numele funcției
Setați numele funcției principale

--id de proprietate
Verificați numai anumite proprietăți cu identificatorul dat

--doar program
Arată doar expresia programului

--adâncimea nr
Limitați adâncimea de căutare

--unwind nr
Derulați bucle de nr ori

--unwindset L:B,...
Derulați bucla L cu o limită de B (utilizați --show-loops pentru a obține ID-urile buclei)

--show-vcc
Afișați condițiile de verificare

--slice-formula
Eliminați sarcinile care nu au legătură cu proprietatea

--aserțiuni fără derulare
Nu generați afirmații relaxante

--fără-nume-frumoase
Nu simplificați identificatorii

BACKEND OPŢIUNI (cbmc)
--dimacs
Generați CNF în format DIMACS pentru a fi utilizat de solutorii SAT externi

--înfrumuseţa-lacom
Înfrumusețați contraexemplul (euristică lacomă)

--smt1 Subobiective de ieșire în sintaxa SMT1 (experimental)

--smt2 Subobiective de ieșire în sintaxa SMT2 (experimental)

--boolector
Utilizați Boolector (experimental)

--mathsat
Utilizați MathSAT (experimental)

--cvc Utilizați CVC3 (experimental)

--jices
Utilizați Yices (experimental)

--z3 Utilizați Z3 (experimental)

--rafina
Utilizați procedura de rafinare (experimental)

--outfile nume de fișier
Formula de ieșire în fișierul dat

--arrays-uf-never
Nu transforma niciodată matricele în funcții neinterpretate

--arrays-uf-intotdeauna
Transformați întotdeauna matricele în funcții neinterpretate

MEDIUL

Toate instrumentele onorează variabila de mediu TMPDIR atunci când generează fișiere temporare și
directoare. Mai mult, rețineți că preprocesorul utilizat de CBMC va folosi mediul
variabile pentru a localiza fișierele antet. GOTO-CC își propune să accepte toate variabilele de mediu care
GCC face.

DREPTURI DE AUTOR

2001-2014, Daniel Kroening, Edmund Clarke

Utilizați goto-cc online folosind serviciile onworks.net