On Mon, Dec 21, 2009 at 9:35 AM, Mauro Baluda <mauro.baluda at unisi.ch> wrote: > is it possible in Klee to have something like > > int n; > klee_make_symbolic(&n, sizeof(n), "n"); > int a[n]; > klee_make_symbolic(a, sizeof(a), "a"); > > I get the error "concretized symbolic size" > is it possible to have ?symbolic sized objects? > CREST seems to be able to manage them
Not currently, no. Handling symbolic sized objects correctly (from my standards of correctness, which are high) is pretty difficult. Currently the best option is to use an arbitrary upper bound, and assert (or klee_assume) that N is less than that bound. An intermediate solution would be to support a subset of the symbolic size problem, by handling the arbitrary upper bound internally. - Daniel > Mauro > -- > Computer science is no more about computers than astronomy is about telescopes > ? ?- Edsger W. Dijkstra > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >
