Hi klee-dev members,
I made args symbolic and provided a seed ktest file for the following target
(code snippets):
if (*(u64*)args >= 0x327b2000 && *(u64*)args <= 0x643c9000) {
printf("WRITE\n");
*(u64*)*(u64*)args = 4;
printf("val1 = %llx\n", *(u64*)args);
printf("point_to1 = %p\n",
ck, Martin
Sent: Tuesday, May 11, 2021 7:33 PM
To: Liu, Mingyi
Cc: klee-dev
Subject: Re: [klee-dev] question on different outputs when running under klee
and with ktest file
Hi Mingyi,
You’ve hit a bug in KLEE.
Thanks for your detailed description - I just opened PR based on your test
Hi klee-dev members,
I made a simple program below and observed different outputs when running under
klee and verifying with the ktest file.
#include
#include "klee/klee.h"
int main() {
int a;
int b;
int c;
klee_make_symbolic(, sizeof(a), "a");
klee_make_symbolic(, sizeof(b),
fferent outputs when running under klee
and with ktest file
Hi,
On Thu, 1 Apr 2021 22:15:57 +
"Liu, Mingyi" wrote:
> printf("%s%s%n\n", , , );
Is this bogus line relevant?
> To be specific, I used the following commands and got three
> paths/testcases as
Hi all,
Could anyone help me understand the following differences?
Thanks,
Mingyi
From: klee-dev-boun...@imperial.ac.uk on
behalf of Liu, Mingyi
Sent: Thursday, April 1, 2021 6:15 PM
To: klee-dev@imperial.ac.uk
Subject: [klee-dev] question on different
Hi klee-dev members,
I made a pointer symbolic in a program, but I didn't understand why the results
were different with the following two scenarios.
Case 1:
#include "klee/klee.h"
#include
#include
#include
#include
int main(int argc, char* argv[]) {
int* ptr;
klee_make_symbolic(,
