Hi all,

Could anyone help me understand the following differences?


Thanks,
Mingyi

________________________________
From: klee-dev-boun...@imperial.ac.uk <klee-dev-boun...@imperial.ac.uk> on 
behalf of Liu, Mingyi <mingyi...@gatech.edu>
Sent: Thursday, April 1, 2021 6:15 PM
To: klee-dev@imperial.ac.uk <klee-dev@imperial.ac.uk>
Subject: [klee-dev] question on different outputs when running under klee and 
with ktest file

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 <stdio.h>
#include "klee/klee.h"

int main() {

  int a;
  int b;
  int c;

  klee_make_symbolic(&a, sizeof(a), "a");
  klee_make_symbolic(&b, sizeof(b), "b");
  klee_make_symbolic(&c, sizeof(c), "c");

  printf("before: a = %d b = %d c = %d\n", a, b, c);

  if (a == 2 && b == 3) {
    printf("%s%s%n\n", &a, &b, &c);
    printf("after: a = %d b = %d c = %d\n", a, b, c);
  }

  return 0;

}

To be specific, I used the following commands and got three paths/testcases as 
expected. What I am confused about is the output for the c value ("after: a = 2 
b = 3 c = 0"), should that be 2? Why it is 0 here?

command: $ clang-9 -I ../klee/include -c -emit-llvm -g -O0 logic_or.c
                  $ ../klee/build/bin/klee -external-calls=all logic_or.bc
[cid:4493b7ad-e1f8-433a-acfd-1f0477862675]

I then compiled the program and ran it with the third testcase above, the 
results are all as expected as c is 2 this time.
command: $ gcc -I ../klee/include logic_or.c -lkleeRuntest -L ../klee/build/lib 
-o logic_or
                  $ KTEST_FILE=klee-last/test000003.ktest ./logic_or
[cid:10eb545b-fc10-4eaf-95ef-062b4f7247f4]


Could you please explain why the output values for c are different? Is it 
intended?



klee version information:

KLEE 2.3-pre (https://klee.github.io)
  Build mode: RelWithDebInfo (Asserts: ON)
  Build revision: 36780583dd78865100114b02627a3418b2d56deb

LLVM (http://llvm.org/):
  LLVM version 9.0.1

  Optimized build.
  Default target: x86_64-pc-linux-gnu
  Host CPU: skylake

Thanks,
Mingyi
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to