Re: [klee-dev] why do I get a very low value of BCov / branch coverage

, you'll see that there is additional code being > linked by KLEE, which is unreachable from main(). If you want to obtain > coverage at the source code level, you need to replay the generated test > cases and use gcov, as explained in the tutorials. > > Best, > Cristian > &

Re: [klee-dev] why do I get a very low value of BCov / branch coverage

2016 at 18:31, Martin Nowack <martin_now...@tu-dresden.de> wrote: > Hi Sumit, > > How did you execute KLEE? What are the parameters? > > Cheers, > Martin > > On 17 May 2016, at 20:44, Sumit Kumar <sumit686...@gmail.com> wrote: > > > > Hi E

[klee-dev] why do I get a very low value of BCov / branch coverage

Hi Everyone, I am getting a BCov value of 22 % for the bitcode input corresponding to the following program although all the branches seem to have been taken: int x; int y; int z; klee_make_symbolic(, sizeof(x), "x"); klee_make_symbolic(, sizeof(y), "y");

Re: [klee-dev] how to add label to assert statements

Hi Dan, On 29 April 2016 at 14:30, Dan Liew <d...@su-root.co.uk> wrote: > Hi, > > On 29 April 2016 at 06:55, Sumit Kumar <sumit686...@gmail.com> wrote: > > Hi Dan, > > > > Thanks for introducing the z3 support. It has been great help. It has > saved >

Re: [klee-dev] how to add label to assert statements

Regards, Sumit On 29 April 2016 at 02:19, Dan Liew <d...@su-root.co.uk> wrote: > Hi, > > On 28 April 2016 at 20:57, Sumit Kumar <sumit686...@gmail.com> wrote: > > Hi, > > I forgot to add this earlier and I think that this is important in this > > context: I

Re: [klee-dev] how to add label to assert statements

<< ":named a" << getAssertNum() << ")"; > *p << " )"; > //*p << ")"; > p->breakLineI(); > } > } > > The function getAssertNum() gets the next identifier for the label. So > using this function, you can gen

Re: [klee-dev] how to add label to assert statements

;)"; > *p << " )"; > //*p << ")"; > p->breakLineI(); > } > } > > The function getAssertNum() gets the next identifier for the label. So > using this function, you can generate query in which assert statements have > labels like a0, a1, a2

[klee-dev] how to add label to assert statements

Hi, Can anyone please tell me how to add label to each of the assert statements in the smt2lib formula emitted by KLEE when getConstraintLog method in Executor.cpp is called with logFormat=STP ? Even if anyone has a faint idea of how it can be done please tell. P.S:This will help me to get an

Re: [klee-dev] meaning of description of the getValue method

ate "expression" into a constant, which is the "result" > argument of getValue(), > and then getValue() returns "true". > > Best, > Andrew > > > > On Sunday, 24 April 2016, 17:53, Sumit Kumar <sumit686...@gmail.com> > wrote: > >

[klee-dev] purpose of conditionals in fork method

Hi, Can anyone please tell me what these conditionals in the fork method in Executor.cpp do: if (!isSeeding && !isa(condition) && (MaxStaticForkPct!=1. || MaxStaticSolvePct != 1. || MaxStaticCPForkPct!=1. || MaxStaticCPSolvePct != 1.) && statsTracker->elapsed() > 60.) {

[klee-dev] meaning of description of the getValue method

Hi All, Can anyone please explain me the meaning of following description of the getValue method described in Solver.cpp: ///getValue - Compute one possible value for the given expression. /// /// \param [out] result - On success, a value for the expression in some /// satisfying

[klee-dev] does the newly created state share anything with its sibling

Hi, Can anyone please tell me that when a state is forked does the newly created state share anything with its sibling or is everything a deep copy. -- Thanks and Regards, Sumit ___ klee-dev mailing list klee-dev@imperial.ac.uk

[klee-dev] how KLEE handles variable scoping

Hi, Can anyone please tell how KLEE handles variable scoping ? -- Thanks and Regards, Sumit Kumar ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[klee-dev] please explain the comments for NotOptimized Kind

Hi, I was reading Expr.h file and I came across the following defined in class Expr: enum Kind{ . . . /// Prevents optimization below the given expression. Used for /// testing: make equality constraints that KLEE will not use to /// optimize to concretes.

Re: [klee-dev] how to introduce a new symbolic variable

nd Regards, Sumit On 5 April 2016 at 03:38, Dan Liew <d...@su-root.co.uk> wrote: > On 4 April 2016 at 15:34, Sumit Kumar <sumit686...@gmail.com> wrote: > > Hi, > > > > Can anyone please tell me how to introduce a new (not declared in test > > program) symb

[klee-dev] Steps required for adding expr

Hi, I was reading Expr.h file when I came across this comment: Steps required for adding an expr: -# Add case to printKind -# Add to ExprVisitor -# Add to IVC (implied value concretization) if possible Can anyone please explain the above in anyway possible

[klee-dev] how to introduce a new symbolic variable

Hi, Can anyone please tell me how to introduce a new (not declared in test program) symbolic variable from within KLEE. -- Thanks and Regards, Sumit ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[klee-dev] KLEE generated only one path whereas program has two

Hi, I tried the latest version (1.2.0) of KLEE using docker. I used the following program: #include #include "../../klee_src/include/klee/klee.h" int main(){ int a; int x; klee_make_symbolic(, sizeof(a), "a"); klee_make_symbolic(, sizeof(x), "x"); a =

Re: [klee-dev] what the third argument in SpecialFunctionHandler::handleMakeSymbolic

what is going wrong here. -- Thanks and Regards Sumit On 19 March 2016 at 18:06, Dan Liew <d...@su-root.co.uk> wrote: > On 19 March 2016 at 10:23, Sumit Kumar <sumit686...@gmail.com> wrote: > > Hi, > > > > Can anyone please explain what the third

[klee-dev] how can I extract the name and index of the array

Hi, Consider the following three lines from LLVM IR: %6 = load i32* %x, align 4 %7 = getelementptr inbounds [10 x i32]* %n, i64 0, i64 2 store i32 %6, i32* %7, align 4 In above code, 'n' is an integer array. Can anyone please tell me that when the store instruction is processed in

[klee-dev] how to clone an expression

Hi, Can anyone please tell me how to clone an expression. I want to get a copy of given expression but they must not share any object. -- Thanks and Regards, Sumit ___ klee-dev mailing list klee-dev@imperial.ac.uk

Re: [klee-dev] where is the class for "EqExpr" located

SS(Eq) > > Which actually declares EqExpr. > > Best, > Andrew > > > On Thursday, 24 March 2016, 4:18, Sumit Kumar <sumit686...@gmail.com> > wrote: > > > Hi, > Can anyone please tell me where is the class for "EqExpr" located. I tried > to find

[klee-dev] static variable that should be accessible from any method

Hi, I want to declare a static variable that should be accessible from any method defined in any of the classes in klee/lib/Core. Where should I declare / define such a variable. -- Thanks and Regards, Sumit ___ klee-dev mailing list

[klee-dev] how the memory is modelled in KLEE

Hi, Can anyone please explain in brief how the memory is modelled in KLEE. Specifically what the classes MemoryObject and ObjectState represent and how they are associated with each other. -- Thanks and Regards Sumit ___ klee-dev mailing list

[klee-dev] convert a non-symbolic variable to symbolic

Hi, Please help: How can I convert a non-symbolic variable (i.e the variable is not declared symbolic in the input program) to symbolic in KLEE. -- Thanks and Regards Sumit ___ klee-dev mailing list klee-dev@imperial.ac.uk

[klee-dev] How can I get KLEE to generate constraints from within function calls

Hi, My test program is this: I declare 'x' as symbolic and then pass the address / value of x as argument to function foo like foo(x) or foo(). Inside the function foo no variables have been explicitly made symbolic. Now when I run KLEE I do not see any constraints generated from foo. How can I

[klee-dev] how to get this constraint in klee

Hi, Can anyone please help me. This is what I want to do in KLEE: 'x', 'y' are integer symbolic variables. Now the following statement is executed: x = y; If after this statement any constraint in KLEE involves x then the value of x is taken as: "ReadLSB w32 0 y" but I want that