goto-cc - Online in de cloud

PROGRAMMA:

NAAM

cbmc - Bounded Model Checker voor C/C++- en Java-programma's

KORTE INHOUD

cbmc [--eigendom eigenschap-id] bestand.c ...

cbmc [--show-eigenschappen] bestand.c ...

cbmc [--alle eigenschappen] bestand.c ...

ga naar cc [-L include-pad] [-C] bestand.c [-of outfile.o]

ga naar instrument in bestand uitbestand

Alleen de meest bruikbare opties worden hier vermeld; zie hieronder voor de rest.

PRODUCTBESCHRIJVING

cbmc genereert sporen die aantonen hoe een bewering geschonden kan worden, of bewijst dat
de bewering kan niet worden geschonden binnen een bepaald aantal lus-iteraties. CBMC kan lezen
broncode rechtstreeks, of een goto-binair gegenereerd door goto-cc. Java-programma's worden gegeven als
klasse bestanden. Zonder verdere opties controleert cbmc alle eigenschappen (automatisch
gegenereerd of door de gebruiker gespecificeerd) gevonden in het programma. Als een van de eigenschappen kan zijn
geschonden, wordt een tegenvoorbeeld afgedrukt en wordt de analyse afgebroken. De analyse kan zijn
beperkt tot een bepaalde eigenschap met de optie --property. Het verificatie resultaat
voor alle eigenschappen kan worden verkregen door middel van de optie --all-properties.

ga naar cc leest de broncode en genereert een goto-binary. De opdrachtregelinterface is
ontworpen om die van na te bootsen gcc(1). Merk vooral op dat ga naar cc maakt onderscheid tussen
fasen samenstellen en koppelen, net zoals gcc dat doet. cbmc verwacht een goto-binary waarvoor
koppeling is voltooid.

ga naar instrument leest een goto-binary, voert een bepaalde programmatransformatie uit, en dan
schrijft het resulterende programma als goto-binary op schijf.

De gebruikelijke manier is om (1) de bron te vertalen in een goto-binair bestand met behulp van goto-cc, en vervolgens (2)
voer instrumentatie uit met goto-instrument, en ten slotte (3) voer de analyse uit met
cbmc.

OPTIES

VOORKANT OPTIES (cbmc en ga naar cc)
-Ik pad
Inclusief pad instellen (C/C++)

-D-macro
Preprocessor-macro definiëren (C/C++)

--voorverwerken
Stop na voorbewerking

--toon-symbool-tabel
Toon symbolentabel

--show-goto-functies
Toon ga naar programma

ARCHITECTURAL OPTIES (cbmc en ga naar cc)
cbmc gebruikt standaard architecturale instellingen die overeenkomen met die van de machine cbmc is
uitgevoerd op, dwz de onderstaande instellingen zijn alleen nodig bij het verifiëren van software
bedoeld om op een andere architectuur of besturingssysteem te draaien. ga naar cc genereert een goto-binair getal voor a
bepaalde architectuur, dwz de architectuur kan niet worden gewijzigd nadat de goto-binary is
gegenereerd.

--16, --32, --64
Stel breedte van int

--LP64, --ILP64, --LLP64, --ILP32, --LP32
Stel de breedte van int, long en pointers in

--klein-endian
Little-endian word-byte conversies toestaan

--big-endian
Sta big-endian word-byte conversies toe

--Ongetekend char
Maak "char" standaard ongetekend

--arch Doelarchitectuur instellen

--os Doelbesturingssysteem instellen

--geen boog
Stel geen architectuur op

--geen-bibliotheek
Schakel ingebouwde abstracte C-bibliotheek uit

--round-to-dichtstbijzijnde, --round-to-plus-inf, --round-to-minus-inf, --round-to-zero
IEEE floating point afrondingsmodus om te gebruiken wanneer het programma begint (standaard is round
naar dichtstbijzijnde). Het te verifiëren programma kan deze instelling overschrijven, bijvoorbeeld met
feestrondje(3).

PROGRAMMA INSTRUMENTATIE OPTIES (cbmc en ga naar instrument)
Te gebruiken zowel cbmc en ga naar instrument kan beweringen genereren die specifieke veelvoorkomende fouten opsporen,
zoals hieronder vermeld.

--grenscontrole
Schakel arraygrenzencontroles in

--div-door-nul-check
Schakel deling door nul-controles in

--aanwijzercontrole
Aanwijzercontroles inschakelen

--ondertekende-overloop-controle
Rekenkundige over- en onderloopcontroles inschakelen voor rekenen met gehele getallen met teken

--unsigned-overflow-check
Schakel rekenkundige over- en onderloopcontroles in voor rekenen met gehele getallen zonder teken

--nan-check
Controleer drijvende-kommaberekeningen voor NaN

--geen-beweringen
Negeer door de gebruiker verstrekte beweringen

--geen aannames
Negeer door de gebruiker verstrekte aannames

--foutlabel label
Controleer of het gegeven label onbereikbaar is

PROGRAMMA INSTRUMENTATIE OPTIES (ga naar instrument only)
ga naar instrument ondersteunt verdere, complexere programmatransformaties.

--nondet-vluchtig
Maakt uitlezingen van vluchtige variabelen niet-deterministisch

--isr-functie
Instrumenteert een interrupt-serviceroutine met de opgegeven naam

--mmio Instruments geheugen toegewezen I/O

--nondet-statisch
Variabelen met een statische levensduur worden niet-deterministisch geïnitialiseerd

--dump-c
Voer ANSI-C-broncode uit in plaats van een goto-binair bestand.

BMC OPTIES (cbmc)
--alle-eigenschappen
Rapporteer de status van alle woningen

--show-eigenschappen
Toon alleen woningen

--show-loops
Toon de lussen in het programma

--cover-beweringen
Controleer welke beweringen bereikbaar zijn

--functie naam
Stel de naam van de hoofdfunctie in

--eigenschap-ID
Controleer alleen een specifieke eigenschap met de gegeven identificatie

--alleen programma
Toon alleen programma-expressie

--diepte nr
Beperk de zoekdiepte

--ontspan nr
Ontspan lussen nr keer

--ontwikkelen L:B,...
Wikkel lus L af met een grens van B (gebruik --show-loops om de lus-ID's te krijgen)

--toon-vcc
Toon de verificatievoorwaarden

--slice-formule
Verwijder toewijzingen die geen verband houden met onroerend goed

--geen-afwikkelende-beweringen
Genereer geen aflopende beweringen

--geen-mooie-namen
Vereenvoudig identificaties niet

ACHTERKANT OPTIES (cbmc)
--dimacs
Genereer CNF in DIMACS-indeling voor gebruik door externe SAT-oplossers

--verfraaien-hebzuchtig
Verfraai het tegenvoorbeeld (heuristiek)

--smt1 Subdoelen uitvoeren in SMT1-syntaxis (experimenteel)

--smt2 Subdoelen uitvoeren in SMT2-syntaxis (experimenteel)

--boelector
Boolector gebruiken (experimenteel)

--wiskunde
Gebruik MathSAT (experimenteel)

--cvc Gebruik CVC3 (experimenteel)

--yes
Yices gebruiken (experimenteel)

--z3 Gebruik Z3 (experimenteel)

--verfijnen
Verfijningsprocedure gebruiken (experimenteel)

--outfile bestandsnaam
Formule uitvoeren naar gegeven bestand

--arrays-uf-nooit
Verander nooit arrays in niet-geïnterpreteerde functies

--arrays-uf-altijd
Verander arrays altijd in niet-geïnterpreteerde functies

MILIEU

Alle tools houden rekening met de omgevingsvariabele TMPDIR bij het genereren van tijdelijke bestanden en
mappen. Houd er verder rekening mee dat de door CBMC gebruikte preprocessor omgeving zal gebruiken
variabelen om headerbestanden te lokaliseren. GOTO-CC streeft ernaar alle omgevingsvariabelen te accepteren
GCC wel.

COPYRIGHT

2001-2014, Daniel Kroening, Edmund Clarke

Gebruik goto-cc online met behulp van onworks.net-services