์ด๊ฒ์ Ubuntu Online, Fedora Online, Windows ์จ๋ผ์ธ ์๋ฎฌ๋ ์ดํฐ ๋๋ MAC OS ์จ๋ผ์ธ ์๋ฎฌ๋ ์ดํฐ์ ๊ฐ์ ์ฌ๋ฌ ๋ฌด๋ฃ ์จ๋ผ์ธ ์ํฌ์คํ ์ด์ ์ค ํ๋๋ฅผ ์ฌ์ฉํ์ฌ OnWorks ๋ฌด๋ฃ ํธ์คํ ์ ๊ณต์ ์ฒด์์ ์คํํ ์ ์๋ cbmc ๋ช ๋ น์ ๋๋ค.
ํ๋ก๊ทธ๋จ:
์ด๋ฆ
cbmc - C/C++ ๋ฐ Java ํ๋ก๊ทธ๋จ์ฉ ๊ฒฝ๊ณ ๋ชจ๋ธ ๊ฒ์ฌ๊ธฐ
๊ฐ์
cbmc [--์ฌ์ฐ ์์ฑ ID] ํ์ผ.c ...
cbmc [--ํ์ ์์ฑ] ํ์ผ.c ...
cbmc [--๋ชจ๋ ์์ฑ] ํ์ผ.c ...
goto-cc [-NS ํฌํจ ๊ฒฝ๋ก] [-์จ] ํ์ผ.c [-๋๋ outfile.o]
๊ณ ํ ์ ๊ธฐ ์ธํ์ผ ์์ํ์ผ
๊ฐ์ฅ ์ ์ฉํ ์ต์ ๋ง ์ฌ๊ธฐ์ ๋์ด๋ฉ๋๋ค. ๋๋จธ์ง๋ ์๋๋ฅผ ์ฐธ์กฐํ์ญ์์ค.
๊ธฐ์
cbmc ์ด์ค์ ์ด ์๋ฐ๋ ์ ์๋ ๋ฐฉ๋ฒ์ ๋ณด์ฌ ์ฃผ๋ ์ถ์ ์ ์์ฑํ๊ฑฐ๋ ๋ค์์ ์ฆ๋ช ํฉ๋๋ค.
์ด์ค์ ์ ์ฃผ์ด์ง ๋ฃจํ ๋ฐ๋ณต ํ์ ๋ด์์ ์๋ฐ๋ ์ ์์ต๋๋ค. CBMC๋ ์ฝ์ ์ ์์ต๋๋ค
์์ค ์ฝ๋ ์ง์ ๋๋ goto-cc์ ์ํด ์์ฑ๋ goto-binary. Java ํ๋ก๊ทธ๋จ์ ๋ค์๊ณผ ๊ฐ์ด ์ ๊ณต๋ฉ๋๋ค.
ํด๋์ค ํ์ผ. ์ถ๊ฐ ์ต์ ์์ด cbmc๋ ๋ชจ๋ ์์ฑ์ ํ์ธํฉ๋๋ค(์๋์ผ๋ก
์์ฑ ๋๋ ์ฌ์ฉ์ ์ง์ ) ํ๋ก๊ทธ๋จ์์ ์ฐพ์ ์ ์์ต๋๋ค. ์์ฑ ์ค ํ๋๊ฐ ๋ ์ ์๋ ๊ฒฝ์ฐ
์๋ฐ๋๋ฉด ๋ฐ๋ก๊ฐ ์ธ์๋๊ณ ๋ถ์์ด ์ค๋จ๋ฉ๋๋ค. ๋ถ์์
--property ์ต์ ์ ์ฌ์ฉํ์ฌ ํน์ ์์ฑ์ผ๋ก ์ ํ๋ฉ๋๋ค. ๊ฒ์ฆ ๊ฒฐ๊ณผ
--all-properties ์ต์ ์ ์ฌ์ฉํ์ฌ ๋ชจ๋ ์์ฑ์ ์ป์ ์ ์์ต๋๋ค.
goto-cc ์์ค ์ฝ๋๋ฅผ ์ฝ๊ณ goto-binary๋ฅผ ์์ฑํฉ๋๋ค. ๋ช ๋ น์ค ์ธํฐํ์ด์ค๋ ๋ค์๊ณผ ๊ฐ์ต๋๋ค.
์ ๊ฒ์ ๋ชจ๋ฐฉํ๋๋ก ์ค๊ณ GCC(1). ํนํ goto-cc ~์ ๊ตฌ๋ณํ๋ค
gcc๊ฐ ํ๋ ๊ฒ์ฒ๋ผ ๋จ๊ณ๋ฅผ ์ปดํ์ผํ๊ณ ์ฐ๊ฒฐํฉ๋๋ค. cbmc goto-binary๋ฅผ ๊ธฐ๋ํฉ๋๋ค.
์ฐ๋์ด ์๋ฃ๋์์ต๋๋ค.
๊ณ ํ ์ ๊ธฐ goto-binary๋ฅผ ์ฝ๊ณ ์ฃผ์ด์ง ํ๋ก๊ทธ๋จ ๋ณํ์ ์ํํ ๋ค์
๊ฒฐ๊ณผ ํ๋ก๊ทธ๋จ์ ๋์คํฌ์ goto-binary๋ก ๊ธฐ๋กํฉ๋๋ค.
์ผ๋ฐ์ ์ธ ํ๋ฆ์ (1) goto-cc๋ฅผ ์ฌ์ฉํ์ฌ ์์ค๋ฅผ goto-binary๋ก ๋ณํํ ๋ค์ (2)
goto-instrument๋ก ๊ณ์ธก์ ์ํํ๊ณ ๋ง์ง๋ง์ผ๋ก (3) ๋ค์์ ์ฌ์ฉํ์ฌ ๋ถ์์ ์ํํฉ๋๋ค.
cbmc.
์ต์
FRONTEND ์ต์ (cbmc ๋ฐ goto-cc)
-๋๋ ๊ธธ
ํฌํจ ๊ฒฝ๋ก ์ค์ (C/C++)
-D ๋งคํฌ๋ก
์ ์ฒ๋ฆฌ๊ธฐ ๋งคํฌ๋ก ์ ์(C/C++)
--์ ์ฒ๋ฆฌ
์ ์ฒ๋ฆฌ ํ ์ค์ง
--show-์ฌ๋ณผ-ํ ์ด๋ธ
๊ธฐํธ ํ ์ด๋ธ ํ์
--show-goto-๊ธฐ๋ฅ
goto ํ๋ก๊ทธ๋จ ํ์
๊ฑด์ถ ์ต์ (cbmc ๋ฐ goto-cc)
cbmc ๊ธฐ๋ณธ์ ์ผ๋ก ์์คํ ์ ์ค์ ๊ณผ ์ผ์นํ๋ ์ํคํ ์ฒ ์ค์ ์ ์ฌ์ฉํฉ๋๋ค. cbmc is
์ฆ, ์๋ ์ค์ ์ ์คํ ์ค์ธ ์ํํธ์จ์ด๋ฅผ ํ์ธํ ๋๋ง ํ์ํฉ๋๋ค.
๋ค๋ฅธ ์ํคํ ์ฒ ๋๋ OS์์ ์คํ๋๋ ๊ฒ์ ์๋ฏธํฉ๋๋ค. goto-cc ๋ํ goto-binary๋ฅผ ์์ฑํฉ๋๋ค.
ํน์ ์ํคํ ์ฒ, ์ฆ goto-binary๊ฐ ๋ณ๊ฒฝ๋ ํ์๋ ์ํคํ ์ฒ๋ฅผ ๋ณ๊ฒฝํ ์ ์์ต๋๋ค.
์์ฑ.
--16, --32, --64
int์ ๋๋น ์ค์
--LP64, --ILP64, --LLP64, --ILP32, --LP32
int, long ๋ฐ ํฌ์ธํฐ์ ๋๋น ์ค์
--๋ฆฌํ ์๋์
little-endian ์๋-๋ฐ์ดํธ ๋ณํ ํ์ฉ
--๋น ์๋์
๋น ์๋์ ์๋ ๋ฐ์ดํธ ๋ณํ ํ์ฉ
--๋ถํธ ์๋ ๋ฌธ์
๊ธฐ๋ณธ์ ์ผ๋ก "char"๋ฅผ ๋ถํธ ์๋ ๊ฒ์ผ๋ก ๋ง๋ญ๋๋ค.
--arch ๋์ ์ํคํ ์ฒ ์ค์
--os ๋์ ์ด์ ์ฒด์ ์ค์
--์์น ์์
์ํคํ ์ฒ๋ฅผ ์ค์ ํ์ง ๋ง์ญ์์ค.
--๋ผ์ด๋ธ๋ฌ๋ฆฌ ์์
๋ด์ฅ ์ถ์ C ๋ผ์ด๋ธ๋ฌ๋ฆฌ ๋นํ์ฑํ
--๊ฐ์ฅ ๊ฐ๊น์ด ๊ฐ์ผ๋ก ๋ฐ์ฌ๋ฆผ, --+inf๋ก ๋ฐ์ฌ๋ฆผ, ---inf๋ก ๋ฐ์ฌ๋ฆผ, --XNUMX์ผ๋ก ๋ฐ์ฌ๋ฆผ
ํ๋ก๊ทธ๋จ์ด ์์๋ ๋ ์ฌ์ฉํ IEEE ๋ถ๋ ์์์ ๋ฐ์ฌ๋ฆผ ๋ชจ๋(๊ธฐ๋ณธ๊ฐ์ ๋ฐ์ฌ๋ฆผ
๊ฐ์ฅ ๊ฐ๊น์ด). ํ์ธ ์ค์ธ ํ๋ก๊ทธ๋จ์ ์ด ์ค์ ์ ๋ฌด์ํ ์ ์์ต๋๋ค.
ํ์ ๋ผ์ด๋(3).
ํ๋ก๊ทธ๋จ ์๋จ ์ต์ (cbmc ๋ฐ ๊ณ ํ ์ ๊ธฐ)
๋ชจ๋ cbmc ๋ฐ ๊ณ ํ ์ ๊ธฐ ํน์ ๊ณตํต ์ค๋ฅ๋ฅผ ํฌ์ฐฉํ๋ ์ด์ค์ ์ ์์ฑํ ์ ์์ต๋๋ค.
์ผ๋ก๋ ๋ค์๊ณผ ๊ฐ์ต๋๋ค.
--๊ฒฝ๊ณ ๊ฒ์ฌ
๋ฐฐ์ด ๋ฒ์ ํ์ธ ํ์ฑํ
--div-by-zero-๊ฒ์ฌ
XNUMX์ผ๋ก ๋๋๊ธฐ ํ์ธ ํ์ฑํ
--ํฌ์ธํฐ ๊ฒ์ฌ
ํฌ์ธํฐ ํ์ธ ํ์ฑํ
--์๋ช -์ค๋ฒํ๋ก-ํ์ธ
๋ถํธ ์๋ ์ ์ ์ฐ์ ์ ๋ํ ์ฐ์ ์ค๋ฒํ๋ก ๋ฐ ์ธ๋ํ๋ก ๊ฒ์ฌ ํ์ฑํ
--unsigned-์ค๋ฒํ๋ก-ํ์ธ
๋ถํธ ์๋ ์ ์ ์ฐ์ ์ ๋ํ ์ฐ์ ์ค๋ฒํ๋ก ๋ฐ ์ธ๋ํ๋ก ๊ฒ์ฌ ํ์ฑํ
--๋-์ฒดํฌ
NaN์ ๋ํ ๋ถ๋ ์์์ ๊ณ์ฐ ํ์ธ
--์ด์ค์ ์์
์ฌ์ฉ์ ์ ๊ณต ์ด์ค์ ๋ฌด์
--๊ฐ์ ์์
์ฌ์ฉ์๊ฐ ์ ๊ณตํ ๊ฐ์ ๋ฌด์
--์ค๋ฅ ๋ ์ด๋ธ ๋ ์ด๋ธ
์ง์ ๋ ๋ ์ด๋ธ์ ๋๋ฌํ ์ ์๋์ง ํ์ธํ์ญ์์ค.
ํ๋ก๊ทธ๋จ ์๋จ ์ต์ (๊ณ ํ ์ ๊ธฐ ๋ง ํด๋น)
๊ณ ํ ์ ๊ธฐ ๋ ๋ณต์กํ๊ณ ๋ ๋ณต์กํ ํ๋ก๊ทธ๋จ ๋ณํ์ ์ง์ํฉ๋๋ค.
--nondet-ํ๋ฐ์ฑ
ํ๋ฐ์ฑ ๋ณ์์ ์ฝ๊ธฐ๋ฅผ ๋น๊ฒฐ์ ์ ์ผ๋ก ๋ง๋ญ๋๋ค.
--isr ํจ์
์ง์ ๋ ์ด๋ฆ์ผ๋ก ์ธํฐ๋ฝํธ ์๋น์ค ๋ฃจํด ๊ณ์ธก
--mmio Instruments ๋ฉ๋ชจ๋ฆฌ ๋งคํ I/O
--nondet-์ ์
์ ์ ์๋ช ์ด ์๋ ๋ณ์๋ ๋น๊ฒฐ์ ์ ์ผ๋ก ์ด๊ธฐํ๋ฉ๋๋ค.
--๋คํ-c
goto ๋ฐ์ด๋๋ฆฌ ๋์ ANSI-C ์์ค ์ฝ๋๋ฅผ ์ถ๋ ฅํฉ๋๋ค.
BMC ์ต์ (CBMC)
--๋ชจ๋ ์์ฑ
๋ชจ๋ ์์ฑ์ ์ํ ๋ณด๊ณ
--ํ์ ์์ฑ
์์ฑ๋ง ํ์
--์ผ ๋ฃจํ
ํ๋ก๊ทธ๋จ์ ๋ฃจํ ํ์
--ํ์ง ์ฃผ์ฅ
๋๋ฌ ๊ฐ๋ฅํ ์ด์ค์ ํ์ธ
--ํจ์ ์ด๋ฆ
์ฃผ์ ๊ธฐ๋ฅ ์ด๋ฆ ์ค์
--์์ฑ ID
์ฃผ์ด์ง ์๋ณ์๋ฅผ ๊ฐ์ง ํน์ ์์ฑ๋ง ํ์ธ
--ํ๋ก๊ทธ๋จ ์ ์ฉ
ํ๋ก๊ทธ๋จ ํํ์๋ง ํ์
--๊น์ด ๋ฒํธ
๊ฒ์ ๊น์ด ์ ํ
--ํ๊ธฐ ๋ฒํธ
๋ฃจํ nr ๋ฒ ํ๊ธฐ
--L:B ์ค์ ํด์ ,...
๊ฒฝ๊ณ B๋ก ๋ฃจํ L ํ๊ธฐ(๋ฃจํ ID๋ฅผ ๊ฐ์ ธ์ค๋ ค๋ฉด --show-loops ์ฌ์ฉ)
--show-vcc
ํ์ธ ์กฐ๊ฑด ํ์
--์ฌ๋ผ์ด์ค ๊ณต์
์์ฑ๊ณผ ๊ด๋ จ ์๋ ํ ๋น ์ ๊ฑฐ
--no-unwinding-์ด์ค์
ํด์ ์ด์ค์ ์ ์์ฑํ์ง ๋ง์ญ์์ค.
--์์ ์ด๋ฆ ์์
์๋ณ์๋ฅผ ๋จ์ํํ์ง ๋ง์ญ์์ค
๋ฐฑ์๋ ์ต์ (CBMC)
--๋๋ง์ค
์ธ๋ถ SAT ์๋ฒ์์ ์ฌ์ฉํ DIMACS ํ์์ CNF ์์ฑ
--beautify-ํ์์ค๋ฌ์ด
๋ฐ๋ก๋ฅผ ๋ฏธํํ๋ผ(์์ฌ ํด๋ฆฌ์คํฑ)
--smt1 SMT1 ๊ตฌ๋ฌธ์ ํ์ ๋ชฉํ ์ถ๋ ฅ(์คํ์ )
--smt2 SMT2 ๊ตฌ๋ฌธ์ ํ์ ๋ชฉํ ์ถ๋ ฅ(์คํ์ )
--๋ถ์ธ๋ ํฐ
Boolector ์ฌ์ฉ(์คํ์ )
--mathsat
MathSAT ์ฌ์ฉ(์คํ์ )
--cvc CVC3 ์ฌ์ฉ(์คํ์ )
--yices
Yices ์ฌ์ฉ(์คํ์ )
--z3 Z3 ์ฌ์ฉ(์คํ์ )
--์ ์
์ ์ ์ ์ฐจ ์ฌ์ฉ(์คํ์ )
--outfile ํ์ผ ์ด๋ฆ
์ฃผ์ด์ง ํ์ผ๋ก ์์ ์ถ๋ ฅ
--๋ฐฐ์ด-uf-์ ๋
๋ฐฐ์ด์ ํด์๋์ง ์์ ํจ์๋ก ๋ฐ๊พธ์ง ๋ง์ญ์์ค.
--๋ฐฐ์ด-uf-ํญ์
ํญ์ ๋ฐฐ์ด์ ํด์๋์ง ์์ ํจ์๋ก ๋ณํ
ํ๊ฒฝ
๋ชจ๋ ๋๊ตฌ๋ ์์ ํ์ผ์ ์์ฑํ ๋ TMPDIR ํ๊ฒฝ ๋ณ์๋ฅผ ๋ฐ๋ฅด๊ณ
๋๋ ํ ๋ฆฌ. ๋ํ CBMC์์ ์ฌ์ฉํ๋ ์ ์ฒ๋ฆฌ๊ธฐ๋ ํ๊ฒฝ์ ์ฌ์ฉํฉ๋๋ค.
ํค๋ ํ์ผ์ ์ฐพ๊ธฐ ์ํ ๋ณ์. GOTO-CC๋ ๋ชจ๋ ํ๊ฒฝ ๋ณ์๋ฅผ ๋ฐ์๋ค์ด๋ ๊ฒ์ ๋ชฉํ๋ก ํฉ๋๋ค.
GCC๊ฐ ํฉ๋๋ค.
์ ์๊ถ
2001-2014, ๋ค๋์ ํฌ๋ก๋, ์๋๋จผ๋ ํด๋ผํฌ
onworks.net ์๋น์ค๋ฅผ ์ฌ์ฉํ์ฌ ์จ๋ผ์ธ์ผ๋ก cbmc๋ฅผ ์ฌ์ฉํ์ธ์.