Hi Cristian,
thanks for the hint, I will take a look.
— Yannic
> On 25 Jan 2017, at 16:01, Cristian Cadar <c.ca...@imperial.ac.uk> wrote:
>
> Hi Yannic, you might like to take a look at KATCH:
> http://srg.doc.ic.ac.uk/projects/katch/
> <http://srg.doc.ic.ac.uk/projects/katch/>
>
> The code is available, but unfortunately not integrated into the mainline.
>
> Cristian
>
> On 23/01/17 15:31, Yannic Noller wrote:
>> Hi Jason,
>>
>> thanks, I know the example and you are right: this is probably the
>> fastest way to try my idea. But this means that there is no special
>> option for an target-oriented search, right? For example I do not want
>> to follow paths that cannot reach my specified target line in order to
>> cut down the possible state space. If not, is it easy to implement such
>> a feature in KLEE?
>>
>> Thanks!
>> — Yannic
>>
>>
>>> On 23 Jan 2017, at 14:12, Papapanagiotakis-Bousy, Iason
>>> <iason.papapanagiotakis-bousy...@ucl.ac.uk
>>> <mailto:iason.papapanagiotakis-bousy...@ucl.ac.uk
>>> <mailto:iason.papapanagiotakis-bousy...@ucl.ac.uk>>> wrote:
>>>
>>> Hi Yannic,
>>>
>>> Have you looked into the maze
>>> tutorial https://feliam.wordpress.com/2010/10/07/the-symbolic-maze/
>>> <https://feliam.wordpress.com/2010/10/07/the-symbolic-maze/> ?
>>>
>>> I am no KLEE veteran but here is my suggestion:
>>> If I understand correctly what you are trying to achieve, then you
>>> could use what is shown in the tutorial and at the end instead of
>>> looking at the .ktest files that will have concrete examples, read the
>>> corresponding .kquery files that contain the path constraints.
>>>
>>> (because the tutorial uses an older version of KLEE, constraints are
>>> stored in a .pc instead of .kquery)
>>>
>>> Hope it helps.
>>>
>>> Best regards,
>>> Jason
>>>
>>> *From:* klee-dev-boun...@imperial.ac.uk
>>> <mailto:klee-dev-boun...@imperial.ac.uk>
>>> <mailto:klee-dev-boun...@imperial.ac.uk
>>> <mailto:klee-dev-boun...@imperial.ac.uk>>
>>> [mailto:klee-dev-boun...@imperial.ac.uk
>>> <mailto:klee-dev-boun...@imperial.ac.uk>] *On Behalf Of *Yannic Noller
>>> *Sent:* Monday, January 23, 2017 2:54 PM
>>> *To:* klee-dev@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk>
>>> <mailto:klee-dev@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk>>
>>> *Subject:* [klee-dev] Target-Directed Symbolic Execution with KLEE
>>>
>>> Hi all,
>>>
>>> I would like to create all path conditions (or an under-approximation)
>>> that reach a certain source code line (something like "directed
>>> symbolic execution"). Is there an option in KLEE to do that? Or is
>>> there an extension of KLEE that can do that?
>>>
>>> Any help is very appreciated :)
>>>
>>> Thanks,
>>> Yannic
>>
>>
>>
>> ___
>> klee-dev mailing list
>> klee-dev@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk>
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>> <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>>
>
> ___
> klee-dev mailing list
> klee-dev@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk>
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
