[klee-dev] fork() : creating child processes in KLEE's execution

[Cristian Cadar]

Hi,

KLEE does not use the system call fork() to fork states.  See 
Executor::fork() in the code.

Best,
Cristian

On 23/02/2022 18:40, Pansilu Pitigalaarachchi wrote:
> Hi,
> 
> I would like to check the possible scenarios where KLEE creates a child 
> process.
> 
> 1.My current understanding is that a 'state fork' performed at a branch 
> condition will not result in a real forking of the KLEE process & does 
> not invoke fork() syscall to create a child process of klee. i.e. the 
> 'state forking' described in the original KLEE paper is a process where 
> the objects in klee's memory are updated to create a new state.
> Can I check if this understanding is correct ?
> 
> 2.In code, I encountered some cases where the fork() syscall is invoked.
> lib/Solver/MetaSMTSolver.cpp
> tools/klee-replay/file-creator.c
> tools/klee-replay/klee-replay.c etc
> Can I check if there are any cases where fork() syscall is issued to 
> fork the klee process as a result of 'state forks' in symbolic execution ?
> 
> I went through the mailing list history and some literature/papers on 
> klee, but cout not find a definite answer. I would really appreciate it 
> if someone can help clarify.
> Thanks in advance.
> -- 
> Pansilu Pitigalaarachchi
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev