[klee-dev] How klee deal with index of array is symbolic?

[Andrew Santosa]

 Hi Qingyang,

I think what you want to know is how to solve array constraints, e.g., x > a[x]
in your example. You can have a look at the following paper on STP, which
is one of the backend solvers KLEE uses:
https://ece.uwaterloo.ca/~vganesh/Publications_files/vg2007-STP-CAV.pdf
Section 3 discusses array constraints solving.

Best,Andrew
 
    On Friday, 20 April 2018, 12:51:32 pm GMT+8, Cx Qingyang <qingyangcx2015 at gmail.com> wrote:  
 
 There is a constraints like  x >=0 &&  x < 3 && x > a[x],where a[3] = {1,2,3}I want to know how klee to judge its validity,when a[3] = {4,5,6},its validity is -1and when a[3] = {1,2,3},how to solve a test case.Thanks very muchYours' qingyang_______________________________________________
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