goto-cc - Online sa Cloud

PROGRAMA:

NAME

cbmc - Bounded Model Checker para sa C/C++ at Java programs

SINOPSIS

cbmc [--pag-aari property-id] file.c ...

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

cbmc [--all-properties] file.c ...

goto-cc [-Ako isama-path] [-c] file.c [-alinman outfile.o]

goto-instrumento infile outfile

Ang mga pinakakapaki-pakinabang na opsyon lamang ang nakalista dito; tingnan sa ibaba para sa natitira.

DESCRIPTION

cbmc bumubuo ng mga bakas na nagpapakita kung paano maaaring labagin ang isang assertion, o nagpapatunay na iyon
hindi maaaring labagin ang assertion sa loob ng isang naibigay na bilang ng mga pag-ulit ng loop. Mababasa ang CBMC
direktang source-code, o isang goto-binary na nabuo ng goto-cc. Ang mga programa ng Java ay ibinibigay bilang
mga file ng klase. Nang walang anumang karagdagang mga pagpipilian, sinusuri ng cbmc ang lahat ng mga katangian (awtomatikong
nabuo o tinukoy ng gumagamit) na matatagpuan sa programa. Kung ang alinman sa mga katangian ay maaaring
nilabag, isang counterexample ay naka-print at ang pagsusuri ay aborted. Ang pagsusuri ay maaaring
restricted sa isang partikular na property na may opsyon na --property. Ang resulta ng pag-verify
para sa lahat ng katangian ay maaaring makuha sa pamamagitan ng --all-properties na opsyon.

goto-cc nagbabasa ng source code, at bumubuo ng goto-binary. Ang interface ng command-line nito ay
dinisenyo upang gayahin ang ng gcc(1). Tandaan sa partikular na goto-cc nakikilala sa pagitan
pag-compile at pag-link ng mga yugto, tulad ng ginagawa ng gcc. cbmc inaasahan ang isang goto-binary kung saan
tapos na ang pag-link.

goto-instrumento nagbabasa ng isang goto-binary, nagsasagawa ng isang ibinigay na pagbabago ng programa, at pagkatapos
isinulat ang resultang programa bilang goto-binary sa disc.

Ang karaniwang daloy ay ang (1) isalin ang pinagmulan sa isang goto-binary gamit ang goto-cc, pagkatapos ay (2)
magsagawa ng instrumentasyon gamit ang goto-instrument, at panghuli (3) magsagawa ng pagsusuri gamit ang
cbmc.

Opsyon

PUMILI Opsyon (cbmc at goto-cc)
-Dali ko
Itakda ang isama ang landas (C/C++)

-D macro
Tukuyin ang preprocessor macro (C/C++)

--preprocess
Huminto pagkatapos ng preprocessing

--show-symbol-table
Ipakita ang talahanayan ng simbolo

--show-goto-functions
Ipakita ang goto program

ARKITEKTURA Opsyon (cbmc at goto-cc)
cbmc bilang default ay gumagamit ng mga setting ng arkitektura na tumutugma sa mga nasa makina cbmc is
naisakatuparan sa, ibig sabihin, ang mga setting sa ibaba ay kailangan lamang kapag nagbe-verify ng software na
nilalayong tumakbo sa ibang arkitektura o OS. goto-cc bumubuo ng goto-binary para sa a
partikular na arkitektura, ibig sabihin, ang arkitektura ay hindi mababago pagkatapos ng goto-binary ay
nabuo

--16, --32, --64
Itakda ang lapad ng int

--LP64, --ILP64, --LLP64, --ILP32, --LP32
Itakda ang lapad ng int, mahaba at mga pointer

--maliit-endian
Payagan ang maliit na-endian na word-byte na mga conversion

--big-endian
Payagan ang mga big-endian na word-byte na conversion

--unsigned-char
Gawing hindi nakapirma ang "char" bilang default

--arch Itakda ang target na arkitektura

--os Itakda ang target na operating system

--walang-arko
Huwag mag-set up ng isang arkitektura

--walang-library
Huwag paganahin ang built-in na abstract C library

--round-to-pinakamalapit, --round-to-plus-inf, --round-to-minus-inf, --round-to-zero
IEEE floating point rounding mode na gagamitin kapag nagsimula ang program (ang default ay bilog
sa pinakamalapit). Maaaring i-override ng program sa ilalim ng pag-verify ang setting na ito, hal, sa
fesetroundNa (3).

PROGRAMA PANUTO Opsyon (cbmc at goto-instrument)
Kapwa cbmc at goto-instrumento maaaring makabuo ng mga pahayag na nakakakuha ng mga partikular na karaniwang pagkakamali,
tulad ng nakalista sa ibaba.

--bounds-check
Paganahin ang mga pagsusuri sa hangganan ng array

--div-by-zero-check
Paganahin ang paghahati sa pamamagitan ng zero check

--pointer-check
Paganahin ang mga tseke ng pointer

--signed-overflow-check
I-enable ang arithmetic over- and underflow checks para sa signed integer arithmetic

--unsigned-overflow-check
I-enable ang mga pagsusuri sa over-and underflow ng arithmetic para sa unsigned integer arithmetic

--nan-check
Suriin ang mga floating-point computations para sa NaN

--walang-assertions
Huwag pansinin ang mga assertion na ibinigay ng user

--walang-pagpapalagay
Huwag pansinin ang mga pagpapalagay na ibinigay ng user

--error-label na label
Tingnan kung hindi maabot ang ibinigay na label

PROGRAMA PANUTO Opsyon (goto-instrumento lamang)
goto-instrumento sumusuporta sa higit pa, mas kumplikado, mga pagbabago sa programa.

--nondet-volatile
Ginagawang hindi deterministiko ang mga pagbabasa mula sa mga pabagu-bagong variable

--isr function
Gumagamit ng interrupt service routine na may ibinigay na pangalan

--mmio Instruments memory-mapped I/O

--nondet-static
Ang mga variable na may static na panghabambuhay ay sinisimulan nang hindi tiyak

--dump-c
I-output ang ANSI-C source code sa halip na isang goto binary.

BMC Opsyon (cbmc)
--all-properties
Iulat ang status ng lahat ng property

--show-properties
Ipakita lamang ang mga katangian

--show-loops
Ipakita ang mga loop sa programa

--cover-assertions
Suriin kung aling mga pahayag ang maaabot

--pangalan ng function
Itakda ang pangalan ng pangunahing function

--property id
Suriin lamang ang partikular na property na may ibinigay na identifier

--program-lamang
Ipakita lamang ang expression ng programa

--depth nr
Limitahan ang lalim ng paghahanap

--unwind nr
Mag-unwind ng mga loop nr beses

--unwindset L:B,...
I-unwind ang loop L na may bound na B (gamitin ang --show-loops para makuha ang mga loop ID)

--show-vcc
Ipakita ang mga kundisyon sa pag-verify

--slice-formula
Alisin ang mga takdang-aralin na walang kaugnayan sa ari-arian

--no-unwinding-assertions
Huwag bumuo ng mga nakakapagpabagal na pahayag

--walang-magandang-pangalan
Huwag pasimplehin ang mga identifier

BACKEND Opsyon (cbmc)
--dimacs
Bumuo ng CNF sa DIMACS na format para magamit ng mga external na solver ng SAT

--paganda-matakaw
Pagandahin ang counterexample (matakaw heuristic)

--smt1 Output subgoals sa SMT1 syntax (pang-eksperimento)

--smt2 Output subgoals sa SMT2 syntax (pang-eksperimento)

--boolector
Gumamit ng Boolector (pang-eksperimento)

--mathsat
Gamitin ang MathSAT (pang-eksperimento)

--cvc Gumamit ng CVC3 (pang-eksperimento)

--yices
Gumamit ng Yices (pang-eksperimento)

--z3 Gamitin ang Z3 (pang-eksperimento)

--pinuhin
Gumamit ng pamamaraan ng pagpipino (pang-eksperimento)

--outfile filename
Output formula sa ibinigay na file

--arrays-uf-hindi kailanman
Huwag kailanman gawing mga hindi na-interpret na function ang mga array

--arrays-uf-laging
Palaging gawing mga hindi naiintindihan na function ang mga array

Kapaligiran

Pinararangalan ng lahat ng mga tool ang variable ng kapaligiran ng TMPDIR kapag bumubuo ng mga pansamantalang file at
mga direktoryo. Higit pa rito, tandaan na ang preprocessor na ginagamit ng CBMC ay gagamit ng kapaligiran
mga variable upang mahanap ang mga file ng header. Nilalayon ng GOTO-CC na tanggapin ang lahat ng mga variable ng kapaligiran na
Ginagawa ng GCC.

COPYRIGHT

2001-2014, Daniel Kroening, Edmund Clarke

Gumamit ng goto-cc online gamit ang mga serbisyo ng onworks.net