[klee-dev] The algorithm of Min-Dist-to-Uncovered Searcher

2016-11-02 Thread Chengyu Zhang
could compute the distance between two instructions in KLEE. 2. What's the difference between CovNew and MD2U search heuristic ? Thanks a lot. Chengyu Zhang -- 张枨宇 Chengyu Zhang East China Normal University School of Computer Science and Software Engineering Tel: 18685412181 Mail: dale.

Re: [klee-dev] The algorithm of Min-Dist-to-Uncovered Searcher

2016-11-18 Thread Chengyu Zhang
to 30 ticks rather than every time we do stepInstruction function? Is it because of low efficiency or other reasons? Best regards, Chengyu 2016-11-02 18:00 GMT+08:00 Chengyu Zhang : > Hi all, > > I saw the md2u(Min-Dist-to-Uncovered) search heuristic in KLEE. > In my opinion, md2

Re: [klee-dev] The algorithm of Min-Dist-to-Uncovered Searcher

2016-11-22 Thread Chengyu Zhang
n iterating all instructions. In this way, we may decrease the cost of updating. Is my idea reasonable? Thanks and Cheers, Chengyu 2016-11-21 21:13 GMT+08:00 Martin Nowack : > Hi Chengyu, > > On 18 Nov 2016, at 15:16, Chengyu Zhang > wrote: > > > > But I have a ques

Re: [klee-dev] Information on reproducing exeperimetation on Coreutils.6.10 with Klee.

2016-12-12 Thread Chengyu Zhang
se. >> >> ___ >> klee-dev mailing list >> klee-dev@imperial.ac.uk >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> >> >> > > ___ > klee-dev mailing

Re: [klee-dev] use klee-fp support float

2016-12-29 Thread Chengyu Zhang
Hi, KLEE can't deal with the float in this version. KLEE will convert float to const when meet float. Because of the limited of STP solver (can't deal with the float constraints) , the develop group of KLEE is trying to add Z3 solver support in KLEE. But the feature have not completed yet. Best

[klee-dev] How to limit unrolling loops times

2017-01-04 Thread Chengyu Zhang
; option in "-help-hidden" can deal with the problem (maybe), but it seems doesn't work. Is there any options could deal with the problem? Or if anyone could tell me how to use "-unroll-threshold" option? Thanks forward, Chengyu -- 张枨宇 Chengyu Zhang East China No

Re: [klee-dev] How to limit unrolling loops times

2017-01-15 Thread Chengyu Zhang
ant to look instead at the search > heuristics that KLEE provides, to see if they are good enough for your > purposes. > > Best, > Cristian > > > On 04/01/2017 11:50, Chengyu Zhang wrote: > >> Hi all, >>I want KLEE stops unrolling loop when meet the unrolling l

Re: [klee-dev] (Re)implementing a randomized fork

2017-01-18 Thread Chengyu Zhang
ne wrong would be > appreciated. > > Cheers, > Sean > > ___ > klee-dev mailing list > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > -- 张枨宇 Chengyu Zhang East China Normal Unive

Re: [klee-dev] KLEE: ERROR: error loading program 'pallin.c': Invalid bitcode signature

2017-10-12 Thread Chengyu Zhang
gt; Build mode: RelWithDebInfo (Asserts: TRUE) > > Build revision: unknown > > > LLVM (http://llvm.org/): > > LLVM version 3.4 > > > > Optimized build. > > Built Mar 5 2014 (17:05:10). > > Default target: x86_64-pc-linux-gnu > > Host C

Re: [klee-dev] Questions about getting symbolic execution tree with KLEE

2018-01-02 Thread Chengyu Zhang
there a > tool for this task? > > Thanks in advance, > Zachery > > > > ___ > klee-dev mailing list > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > -- 张枨宇 Chengyu Zhang East China Normal University Schoo