Re: [klee-dev] Error using klee-replay

Hi Sean, this is a KLEE bug. Please open an issue on GitHub, and I'll try to fix it soon. Thanks, Cristian On 12/12/16 17:48, Sean Heelan wrote: Hi all, When trying to use klee-replay to replay a test case I'm getting the following errors: $

[klee-dev] Building constraints with Expr

Hello everyone, I have a question regarding how to build constraints with the Expr class. The question has been asked a while ago here: https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01513.html I am interested to build an Expr constraint given (in the simplest case) something like "x

Re: [klee-dev] Building constraints with Expr

Hi, > I am interested to build an Expr constraint given (in the simplest case) > something like “x == 0”, how would I do that? I presume that `x` refers to a symbolic variable here. KLEE's Expr language works on Arrays rather than plain variables so in order construct the expression you want

Re: [klee-dev] Is possible to mark a function as uninterpreted function?

Hi Javier, On 14 December 2016 at 13:28, Javier Godoy wrote: > Hi! > > Is possible to mark a function as uninterpreted function in Klee? > > Example i need: > > > foo(int a) > { > if( boo(a) > 0) > return 0; > else > return 1; > } > > boo(int x) //I want to