On 2024-09-16 at 23:20-05:00, 陈小玉 wrote:
> Hello guys. I recently read article "Path-based Inductive Synthesis
> for Program Inversion" and found it very insightful. However,
> I have encountered some questions regarding one of the principles
> discussed in the paper about symbolic execution. I a
On 2024-08-25 at 20:34-07:00, Yuzhou Fang wrote:
> On 2024-08-25 at 22:23+09:00, Nguyễn Gia Phong wrote:
> > SMT solver could give up on the constraint, hence the unknown result.
>
> I'm still quite confused by the situations when solvers will give up.
> Does it mean the c
Greetings,
On 2024-08-23 at 14:12-07:00, Yuzhou Fang wrote:
> I see the return values are slightly different. Method `mustBeTrue` will
> merely return true and false while `evaluate` would give an extra
> `unknown`. Could you briefly explain the difference between them?
SMT solver could give up
On 2024-01-31 at 05:07+00:00, TU Haoxin wrote:
> The behavior is that KLEE fails to fork at a branch
> that should be forked with the option --optimize option enabled
> (i.e., --optimize=true). While the --optimize option is disabled
> i.e., --optimize=false), the branch can be successfully forke
Hi,
In lib/Expr/Constraints.cpp I notice
class ExprReplaceVisitor : public ExprVisitor {
public:
Action visitExpr(const Expr &e) override {
if (e == *src) {
return Action::changeTo(dst);
}
return Action::doChildren();
}
Action visitExprPost(const Expr &e) override {
i
On 2023-07-25 at 18:50+05:30, Sailesh Sai Teja wrote:
> So lets say I want to trace the execution path from function
> "functionA" to function "divide", the following is the output
> I am expecting
>
> 1. "functionA && ((x < y) && divide)"
> 2. "functionA && ((y > 0) && divide)"
Since no one gave
On 2023-07-12 at 22:03+01:00, Cristian Cadar wrote:
> On 07/07/2023 06:57, Nguyễn Gia Phong wrote:
> > I notice that ConstraintSet is implemented via std::vector.
> > This make me wonder about the likelihood of duplucated constraints
> > during executions.
>
>
On 2023-07-09 at 20:25+08:00, 尹麓鸣 wrote:
> How should I compile CoreBench using wllvm
> and use KLEE to check CoreBench?
CoreBench essentially provides the error-introducing and -fixing
commits for each bug. Included programs use the GNU Build System,
which warrants neither backward nor forward c
Hi,
I notice that ConstraintSet is implemented via std::vector.
This make me wonder about the likelihood of duplucated constraints
during executions.
Does anyone have any emprical data or experience regarding this aspect?
Regards,
McSinyx
___
klee-dev
On 2023-05-23 at 18:05+01:00, Frank Busse wrote:
> On Tue, 23 May 2023 16:38:25 +0900
> Nguyễn Gia Phong wrote:
> > what are the potential drawbacks of enabling
> > symbolic printf in KLEE's µClibc?
>
> printf has to transform its parameters into strings. This is h
On Tue Feb 9 11:33:00 GMT 2021, Cristian Cadar wrote:
> printf is run concretely by default (you can add -DKLEE_SYM_PRINTF
> when compiling KLEE's uclibc to change this)
Do you recall the reason for that default,
i.e. what are the potential drawbacks of enabling
symbolic printf in KLEE's µClibc?
11 matches
Mail list logo
