Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Batched concolic path constraints retrieval (seed mode) #1560

Closed
zhaoxuyang13 opened this issue Dec 5, 2022 · 1 comment
Closed

Batched concolic path constraints retrieval (seed mode) #1560

zhaoxuyang13 opened this issue Dec 5, 2022 · 1 comment

Comments

@zhaoxuyang13
Copy link

Is your feature request related to a problem? Please describe.
I'm using klee to generate path conditions for millions of inputs.
I try seed-mode, and use the --seed-dir option to give a directory of ktest file as input.
however, KLEE automatically merge these state and generate only houndreds of smt2 constraint files, but i need one smt2 constraint file per input ktest file as output.
I wonder if this is easy to implement ? or can I realize this in current KLEE version?

BTW, I tried use klee to generate constraint for these ktest file one by one, but it's extremly slow, taking me one second to generate only 2~3 outputs.

@ccadar
Copy link
Contributor

ccadar commented Jun 27, 2023

We would need more information to understand what you mean. Please re-open if you can provide a concrete example (program, .ktest files, etc.).

@ccadar ccadar closed this as completed Jun 27, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants