ȥå   Խ ʬ Хåå ź ʣ ̾ѹ   ñ측 ǽ   إ   ǽRSS

С/y-takata/CPAchecker

Last-modified: 2014-02-27 () 15:06:04 (1383d)
Top / С / y-takata / CPAchecker

CPAchecker˴ؤ

CPAchecker - A Software Verification Tool for Configurable Program Analysis

ڥץ

13Τκ

  • ΥƥȥФƤϤ֤ʰ츫?ˡ
$ gcc maxBug.c getInt.c
$ ./a.out
10 20 30
answer=30
$ ./a.out
10 30 20
answer=30
$ ./a.out
30 20 10
answer=30
  • CPAcheckerȤäƸڤUNSAFEȽϤ롣
$ scripts/cpa.sh -predicateAnalysis -setprop cpa.predicate.solver=SMTInterpol maxBug.c
...
Verification result: UNSAFE. Error path found by chosen configuration.
...
  • report-generator.py Ȥäƥݡ (ErrorPath.0.html) 顼ϩĴ٤롣
$ python scripts/report-generator.py
$ open -a Firefox output/ErrorPath.0.html
  • Ф ErrorPath.0.html
    • 츫ǤϤ狼ˤ(a > b), !(b > c), (x = c), !(x >= a) Ȥϩˤäƥ顼֤ã뤳ȤƤ롣
    • Ĥޤꡤ4Ĥ򤹤٤ a, b, ca > c >= b Ǥ a, b, cˤ¸ߤ줬Ϥȥ顼֤ã롣
  • 25ܤ b > c a > c ˽CPAcheckerϤľȡSAFE ȽϤ롣

2ʤޤڤǤʤ

󥹥ȡȼ¹

嵭WebȤ Download / Installation 顣Mac OS XξUNIXѥХʥɤФ褤

v1.3Java 7ɬܤˤʤäJava 6ʤv1.2ɤ뤳ȡ

ࡦŸ

$ tar xzf CPAchecker-1.3-unix.tar.bz2
$ cd CPAchecker-1.3-unix

¹

$ scripts/cpa.sh -predicateAnalysis -setprop cpa.predicate.solver=SMTInterpol doc/examples/example.c

Mac OS XSMTФ MathSAT 5 Ȥʤ*1ΤǡSMTInterpol Ȥ褦ꤷƤSMTInterpolΤ lib/java/ ƱƤˡ

ޥɥ饤ǻꤹˡconfig/predicateAnalysis.properties ˰ʲιԤɲäƤΤǤ褤

cpa.predicate.solver=SMTInterpol

ϥץ

predicateAnalysis ʤ֤˰ɸŪʲϤԤץ-Analysis ץꤹȡconfig/Analysis.properties ˽äϤԤ롣

README.txt ˺ɬפʤȤ񤫤ƤΤǻȡ

ϥݡȤ

output/* ˽Ϥ줿 HTML ȲѴ롣graphviz (dotޥ) Python 2.7 ɬ*2ܤ doc/BuildReport.txt 򻲾ȡ

$ python scripts/report-generator.py
$ open -a Firefox output/report.html

SafariǤ⸫뤬饤ɥСˤ̾Ǥʤ

оݥץ뽸

¿θоݥץ򽸤᤿ΤƤ롣

Subversionݥȥ꤫åȤ롣

$ svn co https://svn.sosy-lab.org/software/cpachecker/trunk/test

¹

scripts/benchmark.py Linux˶¸ƤΤ*3Mac OS X Ǽ¹ԤΤϺ

SAFE / UNSAFE η̤С㤨аʲΤ褦ʥץȤ¹Ԥ롣

$ for i in test/programs/benchmarks/locks/*.c
  do
    echo -n `basename $i`'  ' 
    scripts/cpa.sh -predicateAnalysis -setprop cpa.predicate.solver=SMTInterpol -noout $i 2>&1 |
    grep result | awk '{print $3}'
  done
test_locks_10_true-unreach-label.c  SAFE.
test_locks_11_true-unreach-label_false-termination.c  SAFE.
test_locks_12_true-unreach-label_false-termination.c  SAFE.
test_locks_13_true-unreach-label.c  SAFE.
test_locks_14_false-unreach-label.c  UNSAFE.
test_locks_14_true-unreach-label.c  SAFE.
test_locks_15_false-unreach-label.c  UNSAFE.
test_locks_15_true-unreach-label_false-termination.c  SAFE.
test_locks_5_true-unreach-label_false-termination.c  SAFE.
test_locks_6_true-unreach-label_false-termination.c  SAFE.
test_locks_7_true-unreach-label_false-termination.c  SAFE.
test_locks_8_true-unreach-label_false-termination.c  SAFE.
test_locks_9_true-unreach-label.c  SAFE.

ξ硤ERROR٥ؤãǽĴ٤ƤΤǡե̾ true-unreach-label ȤΤ SAFEfalse-unreach-label ȤΤ UNSAFE*4

nooutץ output/* ؤνϤ롣


*1 LinuxѤˤMathSAT 5 APIJavaƤӽФɤ°Ƥ뤬MacѤϤʤSnow LeopardǤϥ뤳Ȥ⤦ޤʤä
*2 ȤMacPortsǥ󥹥ȡǽPython 2.7python27Ȥݡ̾python2.7 Ȥޥ̾ǥ󥹥ȡ뤵Τǡθ port select --set python python27 ¹ԤФ褤
*3 cgroupsȤƤ
*4 locks/*.c ˤĤơե̾οϵϡʥåθĿˡ515Ĥλ񸻤ФơŪˤΤĤlockunlock򷫤֤lockƤʤΤunlockȥ顼Ūˤ롼פλ뤬̵¤˽λʤǽ¸ߤ롣

źեե: filegetInt.c 273 [ܺ] filemaxArraySafe.c 249 [ܺ] filemaxArrayFor.c 255 [ܺ] filemaxArray.c 260 [ܺ] filemaxBug.c 313 [ܺ]