[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] 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: $ ./Documents/git/klee/Release+Asserts/bin/klee-rep

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 yo

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 mark this as uninterpre

Re: [klee-dev] Building constraints with Expr

Hi Dan, Thank you very much for the detailed response, the information you provided is hopefully all I need to implement what I am looking for. Regards, Jason From: Dan Liew Sent: 16 December 2016 19:56 To: Papapanagiotakis-Bousy, Iason

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

libm functions such as sin() are 1) usually side-effect free and 2) on floating-point values, which are not typically used for control decision, so many of them can probably be shown statically to not affect branch decision. But let us think about the purpose of symbolicizing them: 1. Since t