Takatalab
¥á¥ó¥Ð¡¼/y-takata/CPAchecker
¤ò¥Æ¥ó¥×¥ì¡¼¥È¤Ë¤·¤ÆºîÀ®
³«»Ï¹Ô:
*CPAchecker¤Ë´Ø¤¹¤ë¥á¥â [#j4f0fda2]
[[CPAchecker - A Software Verification Tool for Configura...
- [[BLAST:http://www.sosy-lab.org/%7Edbeyer/Blast/index-e...
-- C¥½¡¼¥¹¥³¡¼¥É¤ò¸¡¾ÚÂоݤȤ¹¤ë¡£
-- CEGAR (counterexample-guided abstraction refinement) -...
-- cf. Beyer, D. et al., "[[The software model checker BL...
-¤¤¤í¤¤¤í¤Ê²òÀÏË¡¡ÊÎ㤨¤Ðshape analysis¡Ë¤òÁȤ߹ç¤ï¤»¤Æ»È...
**¸¡¾Ú¥µ¥ó¥×¥ë [#example]
***Îã1¡§3¿ô¤Î¤¦¤Á¤ÎºÇÂçÃÍ [#z0082a93]
-Îã¥×¥í¥°¥é¥à: &ref(maxBug.c);
-- ¥Æ¥¹¥È¼Â¹Ô¤·¤¿¤¤¾ì¹ç¤Ï¼¡¤Î¥×¥í¥°¥é¥à¤È¥ê¥ó¥¯¤¹¤ì¤Ð¤è¤¤¡£
--- &ref(getInt.c);
-²¼µ¤Î¥Æ¥¹¥È¥±¡¼¥¹¤ËÂФ·¤Æ¤Ï¤¤¤º¤ì¤âÀµ¤·¤¤Åú¤òÊÖ¤¹¡Ê°ì¸«...
$ 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.predica...
...
Verification result: UNSAFE. Error path found by chosen ...
...
-report-generator.py ¤ò»È¤Ã¤Æ¥ì¥Ý¡¼¥È (ErrorPath.0.html) ...
$ python scripts/report-generator.py
$ open -a Firefox output/ErrorPath.0.html
-¤³¤ÎÎã¤ËÂФ¹¤ë [[ErrorPath.0.html:http://www.info.kochi-...
--°ì¸«¤Ç¤Ï¤ï¤«¤ê¤Ë¤¯¤¤¤¬¡¤(a > b), !(b > c), (x = c...
--¤Ä¤Þ¤ê¡¤¤³¤ì¤é¤Î4¤Ä¤ÎÏÀÍý¼°¤ò¤¹¤Ù¤ÆËþ¤¿¤¹ a, b, c¡Êa &g...
-25¹ÔÌܤΠb > c ¤ò a > c ¤Ë½¤Àµ¤·¤ÆCPAchecker¤ËÆþÎÏ...
***Îã2¡§¡Ê¤¦¤Þ¤¯¸¡¾Ú¤Ç¤¤Ê¤¤Îã¡Ë [#r50facf7]
-Îã¥×¥í¥°¥é¥à
--(1) &ref(maxArray.c);
--(2) &ref(maxArrayFor.c);
--(3) &ref(maxArraySafe.c);
-Îã1¤ÈƱ¤¸¤¯¡¤3¿ô¤Î¤¦¤Á¤ÎºÇÂçÃͤòÊÖ¤¹¥×¥í¥°¥é¥à¡£¤¿¤À¤·ÇÛ...
--3¥×¥í¥°¥é¥à¤È¤âƱ¤¸Æ°ºî¤Ç¤¢¤ë¤Î¤Ç¡¤¸¡¾Ú·ë²Ì¤âƱ¤¸¤Ç¤¢¤ë...
**¥¤¥ó¥¹¥È¡¼¥ë¤È¼Â¹Ô [#z983d597]
¾åµWeb¥µ¥¤¥È¤Î Download / Installation ¤«¤é¡£Mac OS X¤Î...
v1.3¤«¤éJava 7¤¬É¬¿Ü¤Ë¤Ê¤Ã¤¿¡£Java 6¤·¤«¤Ê¤¤¾ì¹ç¤Ïv1.2°Ê...
***²òÅࡦŸ³« [#e5256ce2]
$ tar xzf CPAchecker-1.3-unix.tar.bz2
$ cd CPAchecker-1.3-unix
***¼Â¹Ô [#j8ff4454]
$ scripts/cpa.sh -predicateAnalysis -setprop cpa.predica...
Mac OS X¤À¤ÈSMT¥½¥ë¥Ð¤Î [[MathSAT 5:http://mathsat.fbk.eu...
¥³¥Þ¥ó¥É¥é¥¤¥ó¤Ç»ØÄꤹ¤ëÂå¤ï¤ê¤Ë¡¤config/predicateAnalysi...
cpa.predicate.solver=SMTInterpol
***²òÀÏ¥ª¥×¥·¥ç¥ó [#j5dba2a6]
predicateAnalysis ¤¬¡Ê¤¿¤Ö¤ó¡Ë°ìÈÖɸ½àŪ¤Ê²òÀϤò¹Ô¤¦¥ª¥×...
README.txt ¤ËºÇÄã¸ÂɬÍפʤ³¤È¤¬½ñ¤«¤ì¤Æ¤¤¤ë¤Î¤Ç»²¾È¡£
***²òÀÏ¥ì¥Ý¡¼¥È¤ÎÀ¸À® [#le0e6797]
output/* ¤Ë½ÐÎϤµ¤ì¤¿¾ðÊó¤ò HTML ¤È²èÁü¤ËÊÑ´¹¤¹¤ë¡£¤¿¤À¤·...
$ python scripts/report-generator.py
$ open -a Firefox output/report.html
Safari¤Ç¤â¸«¤é¤ì¤ë¤¬¡¤¥¹¥é¥¤¥É¥Ð¡¼¤Ë¤è¤ë³ÈÂç½Ì¾®¤¬¤Ç¤¤Ê...
**¸¡¾ÚÂоݥµ¥ó¥×¥ë½¸ [#vbc8cc08]
¿¤¯¤Î¸¡¾ÚÂоݥµ¥ó¥×¥ë¤ò½¸¤á¤¿¤â¤Î¤¬¸ø³«¤µ¤ì¤Æ¤¤¤ë¡£
***¥À¥¦¥ó¥í¡¼¥É [#t466d257]
Subversion¥ê¥Ý¥¸¥È¥ê¤«¤é¥Á¥§¥Ã¥¯¥¢¥¦¥È¤¹¤ë¡£
$ svn co https://svn.sosy-lab.org/software/cpachecker/tr...
***¼Â¹Ô [#f58bee68]
scripts/benchmark.py ¤ÏLinux¤Ë¶¯¤¯°Í¸¤·¤Æ¤¤¤ë¤Î¤Ç(([[cgr...
SAFE / UNSAFE ¤Î·ë²Ì¤¬ÆÀ¤¿¤±¤ì¤Ð¡¤Î㤨¤Ð°Ê²¼¤Î¤è¤¦¤Ê¥¹¥¯...
$ for i in test/programs/benchmarks/locks/*.c
do
echo -n `basename $i`' '
scripts/cpa.sh -predicateAnalysis -setprop cpa.predi...
grep result | awk '{print $3}'
done
test_locks_10_true-unreach-label.c SAFE.
test_locks_11_true-unreach-label_false-termination.c SA...
test_locks_12_true-unreach-label_false-termination.c SA...
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 SA...
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¥é¥Ù¥ë¤Ø¤ÎÅþã²ÄǽÀ¤òÄ´¤Ù¤Æ¤¤¤ë¤Î¤Ç¡¤¥Õ¥¡...
noout¥ª¥×¥·¥ç¥ó¤Ï output/* ¤Ø¤Î½ÐÎϤòÍÞÀ©¤¹¤ë¡£
½ªÎ»¹Ô:
*CPAchecker¤Ë´Ø¤¹¤ë¥á¥â [#j4f0fda2]
[[CPAchecker - A Software Verification Tool for Configura...
- [[BLAST:http://www.sosy-lab.org/%7Edbeyer/Blast/index-e...
-- C¥½¡¼¥¹¥³¡¼¥É¤ò¸¡¾ÚÂоݤȤ¹¤ë¡£
-- CEGAR (counterexample-guided abstraction refinement) -...
-- cf. Beyer, D. et al., "[[The software model checker BL...
-¤¤¤í¤¤¤í¤Ê²òÀÏË¡¡ÊÎ㤨¤Ðshape analysis¡Ë¤òÁȤ߹ç¤ï¤»¤Æ»È...
**¸¡¾Ú¥µ¥ó¥×¥ë [#example]
***Îã1¡§3¿ô¤Î¤¦¤Á¤ÎºÇÂçÃÍ [#z0082a93]
-Îã¥×¥í¥°¥é¥à: &ref(maxBug.c);
-- ¥Æ¥¹¥È¼Â¹Ô¤·¤¿¤¤¾ì¹ç¤Ï¼¡¤Î¥×¥í¥°¥é¥à¤È¥ê¥ó¥¯¤¹¤ì¤Ð¤è¤¤¡£
--- &ref(getInt.c);
-²¼µ¤Î¥Æ¥¹¥È¥±¡¼¥¹¤ËÂФ·¤Æ¤Ï¤¤¤º¤ì¤âÀµ¤·¤¤Åú¤òÊÖ¤¹¡Ê°ì¸«...
$ 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.predica...
...
Verification result: UNSAFE. Error path found by chosen ...
...
-report-generator.py ¤ò»È¤Ã¤Æ¥ì¥Ý¡¼¥È (ErrorPath.0.html) ...
$ python scripts/report-generator.py
$ open -a Firefox output/ErrorPath.0.html
-¤³¤ÎÎã¤ËÂФ¹¤ë [[ErrorPath.0.html:http://www.info.kochi-...
--°ì¸«¤Ç¤Ï¤ï¤«¤ê¤Ë¤¯¤¤¤¬¡¤(a > b), !(b > c), (x = c...
--¤Ä¤Þ¤ê¡¤¤³¤ì¤é¤Î4¤Ä¤ÎÏÀÍý¼°¤ò¤¹¤Ù¤ÆËþ¤¿¤¹ a, b, c¡Êa &g...
-25¹ÔÌܤΠb > c ¤ò a > c ¤Ë½¤Àµ¤·¤ÆCPAchecker¤ËÆþÎÏ...
***Îã2¡§¡Ê¤¦¤Þ¤¯¸¡¾Ú¤Ç¤¤Ê¤¤Îã¡Ë [#r50facf7]
-Îã¥×¥í¥°¥é¥à
--(1) &ref(maxArray.c);
--(2) &ref(maxArrayFor.c);
--(3) &ref(maxArraySafe.c);
-Îã1¤ÈƱ¤¸¤¯¡¤3¿ô¤Î¤¦¤Á¤ÎºÇÂçÃͤòÊÖ¤¹¥×¥í¥°¥é¥à¡£¤¿¤À¤·ÇÛ...
--3¥×¥í¥°¥é¥à¤È¤âƱ¤¸Æ°ºî¤Ç¤¢¤ë¤Î¤Ç¡¤¸¡¾Ú·ë²Ì¤âƱ¤¸¤Ç¤¢¤ë...
**¥¤¥ó¥¹¥È¡¼¥ë¤È¼Â¹Ô [#z983d597]
¾åµWeb¥µ¥¤¥È¤Î Download / Installation ¤«¤é¡£Mac OS X¤Î...
v1.3¤«¤éJava 7¤¬É¬¿Ü¤Ë¤Ê¤Ã¤¿¡£Java 6¤·¤«¤Ê¤¤¾ì¹ç¤Ïv1.2°Ê...
***²òÅࡦŸ³« [#e5256ce2]
$ tar xzf CPAchecker-1.3-unix.tar.bz2
$ cd CPAchecker-1.3-unix
***¼Â¹Ô [#j8ff4454]
$ scripts/cpa.sh -predicateAnalysis -setprop cpa.predica...
Mac OS X¤À¤ÈSMT¥½¥ë¥Ð¤Î [[MathSAT 5:http://mathsat.fbk.eu...
¥³¥Þ¥ó¥É¥é¥¤¥ó¤Ç»ØÄꤹ¤ëÂå¤ï¤ê¤Ë¡¤config/predicateAnalysi...
cpa.predicate.solver=SMTInterpol
***²òÀÏ¥ª¥×¥·¥ç¥ó [#j5dba2a6]
predicateAnalysis ¤¬¡Ê¤¿¤Ö¤ó¡Ë°ìÈÖɸ½àŪ¤Ê²òÀϤò¹Ô¤¦¥ª¥×...
README.txt ¤ËºÇÄã¸ÂɬÍפʤ³¤È¤¬½ñ¤«¤ì¤Æ¤¤¤ë¤Î¤Ç»²¾È¡£
***²òÀÏ¥ì¥Ý¡¼¥È¤ÎÀ¸À® [#le0e6797]
output/* ¤Ë½ÐÎϤµ¤ì¤¿¾ðÊó¤ò HTML ¤È²èÁü¤ËÊÑ´¹¤¹¤ë¡£¤¿¤À¤·...
$ python scripts/report-generator.py
$ open -a Firefox output/report.html
Safari¤Ç¤â¸«¤é¤ì¤ë¤¬¡¤¥¹¥é¥¤¥É¥Ð¡¼¤Ë¤è¤ë³ÈÂç½Ì¾®¤¬¤Ç¤¤Ê...
**¸¡¾ÚÂоݥµ¥ó¥×¥ë½¸ [#vbc8cc08]
¿¤¯¤Î¸¡¾ÚÂоݥµ¥ó¥×¥ë¤ò½¸¤á¤¿¤â¤Î¤¬¸ø³«¤µ¤ì¤Æ¤¤¤ë¡£
***¥À¥¦¥ó¥í¡¼¥É [#t466d257]
Subversion¥ê¥Ý¥¸¥È¥ê¤«¤é¥Á¥§¥Ã¥¯¥¢¥¦¥È¤¹¤ë¡£
$ svn co https://svn.sosy-lab.org/software/cpachecker/tr...
***¼Â¹Ô [#f58bee68]
scripts/benchmark.py ¤ÏLinux¤Ë¶¯¤¯°Í¸¤·¤Æ¤¤¤ë¤Î¤Ç(([[cgr...
SAFE / UNSAFE ¤Î·ë²Ì¤¬ÆÀ¤¿¤±¤ì¤Ð¡¤Î㤨¤Ð°Ê²¼¤Î¤è¤¦¤Ê¥¹¥¯...
$ for i in test/programs/benchmarks/locks/*.c
do
echo -n `basename $i`' '
scripts/cpa.sh -predicateAnalysis -setprop cpa.predi...
grep result | awk '{print $3}'
done
test_locks_10_true-unreach-label.c SAFE.
test_locks_11_true-unreach-label_false-termination.c SA...
test_locks_12_true-unreach-label_false-termination.c SA...
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 SA...
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¥é¥Ù¥ë¤Ø¤ÎÅþã²ÄǽÀ¤òÄ´¤Ù¤Æ¤¤¤ë¤Î¤Ç¡¤¥Õ¥¡...
noout¥ª¥×¥·¥ç¥ó¤Ï output/* ¤Ø¤Î½ÐÎϤòÍÞÀ©¤¹¤ë¡£
¥Ú¡¼¥¸Ì¾: