[klee-dev] Store path in Klee

[Andrew Santosa]

Dear Chelsea,
I think you may want to explore KLEE's -write-paths, -write-pcs, -write-cvcs, and -weire-smt2s options.-write-paths in particular outputs a sequence of 0s and 1s in a .path file for each test case indicating whetherrespectively it is the false or the true branch that is taken at every branching point.

Best,Andrew 

    On Monday, 12 December 2016, 5:29, Chelsea Metcalf <metcalf.chelsea at gmail.com> wrote:
 

  #yiv1317773325 * a:hover{cursor:pointer;} #yiv1317773325 body {} _filtered #yiv1317773325 {}#yiv1317773325 to {position:relative;}#yiv1317773325   #yiv1317773325 a {word-wrap:normal;}#yiv1317773325 .yiv1317773325background-contain {background-size:contain;}@media screen and (max-width:600px){#yiv1317773325 .yiv1317773325container {}#yiv1317773325 .yiv1317773325container, #yiv1317773325 .yiv1317773325palm-one-whole {width:100% !important;min-width:100% !important;}#yiv1317773325 .yiv1317773325palm-one-half {width:50% !important;min-width:50% !important;}#yiv1317773325 blockquote .yiv1317773325container, #yiv1317773325 blockquote .yiv1317773325container div, #yiv1317773325 blockquote .yiv1317773325container table {width:auto !important;min-width:0 !important;position:relative;}#yiv1317773325 img {max-width:100%;}#yiv1317773325 .yiv1317773325border-outer, #yiv1317773325 .yiv1317773325border-middle, #yiv1317773325 .yiv1317773325border-inner, #yiv1317773325 .yiv1317773325inner, #yiv1317773325 .filtered99999 {width:100% !important;}#yiv1317773325 .yiv1317773325innercell {padding:8px !important;}#yiv1317773325 .yiv1317773325palm-block {display:block;}#yiv1317773325 td.yiv1317773325palm-one-whole {display:inline-block;padding:0;}#yiv1317773325 td.yiv1317773325palm-one-whole:first-child:not {margin-bottom:16px;}#yiv1317773325 td.yiv1317773325hostname {padding-top:3px !important;}}@media screen and (min-width:601px){#yiv1317773325 .yiv1317773325preview-card {max-width:600px !important;}}@media screen and ( _filtered_a )and ( _filtered_a )screen and ( _filtered_a )and ( _filtered_a )screen and ( _filtered_a )screen and ( _filtered_a )screen and ( _filtered_a ){#yiv1317773325 .yiv1317773325container {width:100% !important;min-width:100% !important;}#yiv1317773325 .yiv1317773325p, #yiv1317773325 .yiv1317773325small, #yiv1317773325 li, #yiv1317773325 font .filtered99999 , #yiv1317773325 font .filtered99999 {font-size:1em !important;}}@media screen and ( _filtered_a )and ( _filtered_a )screen and ( _filtered_a )and ( _filtered_a )screen and ( _filtered_a ){#yiv1317773325 .yiv1317773325message-wrapper {padding-top:6px;}#yiv1317773325 .yiv1317773325apple-only .filtered99999 {display:block;max-height:none !important;line-height:normal !important;overflow:visible;height:auto !important;width:100% !important;position:relative;}#yiv1317773325 .yiv1317773325no-apple {display:none;}#yiv1317773325 form {font-size:inherit;}#yiv1317773325 input .filtered99999 {height:43px;padding-left:4px !important;}#yiv1317773325 button:hover {cursor:pointer;}}@media screen and ( _filtered_a ){#yiv1317773325 .yiv1317773325apple-mail-form {display:block;background-color:white;}}#yiv1317773325 * .filtered99999 .yiv1317773325outlook-com-hidden {display:none;}#yiv1317773325 * .filtered99999 .yiv1317773325outlook-com-button {display:block;}#yiv1317773325 * .filtered99999 .yiv1317773325outlook-com-only {display:block;max-height:none !important;line-height:normal !important;overflow:visible;height:auto !important;width:100% !important;position:relative;}#yiv1317773325 .yiv1317773325ExternalClass {width:100%;}#yiv1317773325 .yiv1317773325ExternalClass .yiv1317773325outlook-com-button {display:block;}#yiv1317773325 .yiv1317773325ExternalClass button {height:auto;}#yiv1317773325 .yiv1317773325ExternalClass .yiv1317773325outlook-com-hidden {display:none;}#yiv1317773325 .yiv1317773325ExternalClass .yiv1317773325outlook-com-only {display:block;max-height:none !important;line-height:normal !important;overflow:visible;height:auto !important;width:100% !important;position:relative;}#yiv1317773325 .yiv1317773325ExternalClass .yiv1317773325ecxlabels {display:none;}#yiv1317773325 .yiv1317773325ExternalClass .yiv1317773325ecxlabels {display:none;}#yiv1317773325 .yiv1317773325ExternalClass .yiv1317773325ecxarrow {display:none;}#yiv1317773325 .yiv1317773325ExternalClass cite >div + div {padding:0 0 4px 0;}#yiv1317773325 .yiv1317773325ExternalClass .yiv1317773325h1 {padding-bottom:5px;}#yiv1317773325 .yiv1317773325ExternalClass .yiv1317773325h2 {padding-bottom:5px;}#yiv1317773325 .yiv1317773325ExternalClass .yiv1317773325h3 {padding-bottom:5px;}#yiv1317773325 .yiv1317773325ExternalClass .filtered99999 {width:280px !important;} 
|  Hi,
Is there a way in Klee to store the path that is being taken?
Thanks,Chelsea  |

 
_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


   
-------------- next part --------------
HTML attachment scrubbed and removed