Re: [klee-dev] KLEE cannot be found

On 2 December 2014 at 03:52, Wei Wen wei.w...@gmail.com wrote: Hello, I successfully built KLEE. However, when I followed tutorials to run KLEE, I got error messages saying that KLEE cannot be found. Some people told me that I should find the KLEE executables and link them to my usr/bin

Re: [klee-dev] APint::udiv assertion fails

On 15 December 2014 at 18:13, Dingbao Xie xieding...@gmail.com wrote: Hi, everyone I encountered an assertion failure when trying to test grep with klee. The complete stack trace is shown below: Looks like a division by zero happened whilst evaluating an instruction that uses constants.

Re: [klee-dev] About klee error while compiling

You're missing several things * The -emit-llvm command line argument to clang (the most important thing here, you're not trying to build a native binary here) * -I/path/to/klee_source/include command line argument to clang to clang and in your source a #include klee/klee.h

Re: [klee-dev] Install Problems for LLVM2.9

On 21 January 2015 at 13:33, Zhiyi Zhang xianlingzibiy...@gmail.com wrote: Hello, I encountered a problem when I installed LLVM2.9. The error information is as following: Intercept.cpp:69:67: error: ‘lseek64’ was not declared in this scope sys::DynamicLibrary::AddSymbol(\x1lseek64,

Re: [klee-dev] coreutils on KLEE3.4

Hi Zhiyi, Please do reply-all when using the mailing list so that klee-dev gets CC'ed. On 18 March 2015 at 08:32, Zhiyi Zhang xianlingzibiy...@gmail.com wrote: Hi Dan, Thank you for your reply very much. I am still confused that do you mean coreutills cannot be run on KLEE compiled with

Re: [klee-dev] coreutils on KLEE3.4

On 18 March 2015 at 08:17, Zhiyi Zhang xianlingzibiy...@gmail.com wrote: Hi all, I have built the KLEE3.4 on Ubuntu14.10 and the Tutorial get_sign and Regexp can also be run by KLEE3.4. I used clang to compile programs and run .bc file on KLEE. However, when I built the coreutils on KLEE3.4

Re: [klee-dev] klee with llvm-3.6?

On 22 March 2015 at 21:03, Cristian Cadar c.ca...@imperial.ac.uk wrote: I think there is some rationale for having that code there, as we have found it useful to have finer-grained control over optimisations in KLEE in order to improve performance. You can run all LLVM optimisations outside of

Re: [klee-dev] klee with llvm-3.6?

Hi, There was some discussion about linking in Klee earlier on github (https://github.com/klee/klee/pull/141). My preference is to remove all linking from Klee. A provided wrapper script can do the necessary linking using llvm-link and possibly some opt calls for internalization of functions

Re: [klee-dev] whole-program-llvm

Hi, it reports the error that ERROR:File /home/loveling10/klee/examples/coreutils/coreutils/obj-llvm/src/base64.o of type ELF_OBJECT cannot be used. You're supposed to run ``extract-bc`` on the final executable i.e. ``base64``. You tried running ``extract-bc`` on one of the constituent

Re: [klee-dev] about klee inputs

On 11 March 2015 at 17:13, douglas schroeder dougla...@gmail.com wrote: Hello, thanks for the reply. another question. in my tests, almost all generated inputs are zeros. 0: name: 'string' object0: size: 8 object0: data: '\x00\x00\x00\x00\x00\x00\x00\x00' object1: name: 'data'

Re: [klee-dev] Invalid recordLoading

On 24 March 2015 at 21:16, Alberto Barbaro barbaro.albe...@gmail.com wrote: Hi all, I'm trying to set up klee with llvm 3.4 following the step by step guide. Everything looks good apart the last step. When I execute lit -v . I have this error: Klee-uclibc.bca failed: invalid record loading

Re: [klee-dev] [KLEE-dev] printing queries in SMT2 format

Hi, KLEE already has SMTLIBv2 printing support (I presume that's what you mean by SMT2). It is implemented in the ExprSMTLIBPrinter class [1]. You can tell klee to log in this format using ``--use-query-log=all:smt2``. You can also convert .pc files to SMT-LIBv2 format using the ``kleaver`` tool

Re: [klee-dev] The incorrect result obtained from KLEE (BVTypeCheck: terms in atomic formulas must be of equal length)

Dan, the message starts with We tried two versions of STP (r940 and the latest) :) Yes but - I was asking if you had STP built with assertions when trying to reproduce the issue. It is obvious the the OP had assertions enabled when they ran their build of KLEE. - The stacktrace shown by the

Re: [klee-dev] The incorrect result obtained from KLEE (BVTypeCheck: terms in atomic formulas must be of equal length)

On 27 February 2015 at 10:52, Cristian Cadar c.ca...@imperial.ac.uk wrote: I cannot reproduce this on my machine. Can you open an issue at https://github.com/klee/klee/issues, giving more details on your configuration and how you ran KLEE? Do you have STP built with assertions? They've been

Re: [klee-dev] Dockerizing Klee

Hi, I think it would be useful to have an official repository for the dockerized KLEE, which we would recommend to new users on the KLEE website, and which would be maintained as part of the KLEE project on GitHub (https://github.com/klee). Also, it would be useful to automatically update

Re: [klee-dev] whole-program-llvm

Hi, Exception: Could not find .llvm_bc ELF section in /home/loveling10/klee/examples/coreutils/coreutils/obj-llvm/src/base64 You probably didn't use whole-program-llvm for your compilation process if you see this message. You should check if ``make`` was actually using wllvm, my guess it

Re: [klee-dev] Beginnier to KLEE

Hi, I want to explore symbolic execution and KLEE seems like a good choice for beginning. But I would like you guidance in getting to know the best way to understand the code of KLEE. One thing you certainly do is read the OSDI'08 paper on KLEE to get a high level understanding of what it

Re: [klee-dev] More about all/solver-queries.smt2 files

Hi, On 12 May 2015 at 14:50, Andrea Aquino andrex.aqu...@gmail.com wrote: Dear all, I analyzed the coreutils of the linux kernel using KLEE (llvm version 2.9 on host 1386-pc-linux-gnu (Ubuntu 32 bits)). I configured KLEE to use both caches, to timeout after 1 minute, to produce no output

Re: [klee-dev] error : klee + coreutils + experimental [+docker]

sudo docker run -ti klee/klee klee@2f1c0eaa949c:~$ wget http://ftp.gnu.org/gnu/coreutils/coreutils-6.11.tar.gz klee@2f1c0eaa949c:~$ tar xf coreutils-6.11.tar.gz klee@2f1c0eaa949c:~$ cd coreutils-6.11 klee@2f1c0eaa949c:~/coreutils-6.11$ mkdir obj-gcov cd obj-gcov

Re: [klee-dev] My forked KLEE using LLVM 3.6 passes regression and unit tests

Hi Chase, Thanks for taking this work on. On 15 April 2015 at 20:43, Chace Clark cha...@tamu.edu wrote: I have been working on updating KLEE to work using the newest stable version of LLVM (3.6). It now passes the same regression tests that the llvm 3.4.2 version does, as well as all the

Re: [klee-dev] My forked KLEE using LLVM 3.6 passes regression and unit tests

4. Enable TravisCI tests for LLVM 3.6. Look at the /.travis.yml file. Hopefully it would just be a case of adding a few more configurations the ``env`` key - LLVM_VERSION=3.6 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - LLVM_VERSION=3.6 STP_VERSION=UPSTREAM

Re: [klee-dev] error : klee + coreutils + experimental [+docker]

On 16 April 2015 at 13:59, Joshep J. Cortez Sanchez agne...@gmail.com wrote: Dan, Thanks for answer! In the 1) case, using whole-program-llvm all works fine. Great. I don't know why in the tutorial(step 6) gives: Lines executed:97.03% of 101 and I obtained: Lines executed:97.09% of

Re: [klee-dev] error : klee + coreutils + experimental [+docker]

Hi, Clearly i have not llvm-ld because it was removed. So, what shuold I change in klee-gcc to make it work with the new settings/version of things klee-gcc is only meant to be used with llvm-gcc. I would use whole-program-llvm [1] to build core utils if you are using clang. $ export

Re: [klee-dev] KLEE make pointer symbolically

On 3 June 2015 at 05:28, 张若虚 zhangruoxu0...@qq.com wrote: Hi all, In the following program, I make a pointer symbolically. The name of program file is array.c int main(int argc, char **argv) { int a = 0; int *p = a; klee_make_symbolic(p, sizeof(p), a); *p = 1; return EXIT_SUCCESS; }

Re: [klee-dev] Klee Make Check

Hi, On 22 May 2015 at 01:04, Ben Mehne bme...@berkeley.edu wrote: Hello, I am trying to compile and use Klee with the POSIX/uClibc environment, but make check exits with error and Unexpected Failures: 36. Does this mean that klee will not function as intended? Any guidance would

Re: [klee-dev] structure definition in KLEE source code

Look at Expr.h and Expr.cpp. https://github.com/klee/klee/blob/master/include/klee/Expr.h https://github.com/klee/klee/blob/master/lib/Expr/Expr.cpp If you're looking at adding floating point support consider looking at Peter Collingbourne's fork of KLEE (klee-fp/klee-cl) which extends KLEE's

Re: [klee-dev] KLEE+Z3 (an instance of KLEE-MultiSolver) still concretizes floating point expression to 0.

Is there a way to tell KLEE not to concretieze floating point expression to 0 so KLEE + Z3 can be useful when handling floating point program? Not right now no. KLEE's expression language does not support floating point constraints right now which is why floating point numbers get concretised.

Re: [klee-dev] EasyKLEE

Hi, On 16 August 2015 at 11:02, Owl owl whootandah...@gmail.com wrote: Hey, Wanted to give people a heads up that I've started a project to simplify the install process for KLEE. https://github.com/Owlz/EasyKLEE At the moment, I've only gotten support for Ubuntu 15.04 x64, but am

Re: [klee-dev] Error in configuring KLEE with Ubuntu 12.04 LTS 64-bit

On 2 September 2015 at 09:25, Giuseppe Petracca wrote: > Hi, > I am currently encountering the following error while configuring KLEE > > http://stackoverflow.com/questions/32337845/klee-configuration-error?noredirect=1#comment52581865_32337845 I posted an answer of

Re: [klee-dev] Klee path statistics and merging options

> Is the number of completed paths same as number of feasible paths in the > program ? > > 2> Does Klee invoke a SAT query at every branch point in the program by > default to determine > the eager infeasibility of a path ? Or is there other heuristics to > selectively chose branch points ? AFAIK

Re: [klee-dev] a question about kleaver

Hi, On 8 January 2016 at 10:18, xiaoqixue_1 wrote: > > > Hi, > > When a use kleaver to solve a query, I found that "Ult" and "Ugt" can not be > used at the same time. > the logic is simple: > if( sn > 5) { >if( sn < 8 ) { > if (sn==0) printf("hello"); >

Re: [klee-dev] Klee path statistics and merging options

Hi, On 17 December 2015 at 02:08, RAJDEEP MUKHERJEE wrote: > > Hi, > > I have the following queries regarding Klee. I would really appreciate any > help. > > 1> How to obtain the following statistics from Klee: > A> Total number of feasible paths, > B> Total

Re: [klee-dev] Testing coreutils: Invalid record

On 28 December 2015 at 05:35, felicia wrote: > I followed the instruction on > https://klee.github.io/tutorials/testing-coreutils/ > I would like to run coreutils by using KLEE latest version and LLVM 3.4 > Since, I use clang instead of llvm-gcc. In the step 2, I use

Re: [klee-dev] how KLEE handles variable scoping

On 8 April 2016 at 18:01, Sumit Kumar wrote: > Hi, > > Can anyone please tell how KLEE handles variable scoping ? KLEE executes LLVM IR. Clang is handling the variable scoping here so that KLEE never sees any scoping issues. ___

Re: [klee-dev] How can I get KLEE to generate constraints from within function calls

On 18 March 2016 at 15:00, Sumit Kumar wrote: > Hi, > > My test program is this: I declare 'x' as symbolic and then pass the address > / value of x as argument to function foo like foo(x) or foo(). Inside the > function foo no variables have been explicitly made symbolic.

Re: [klee-dev] how to know if variable is symbolic

On 17 March 2016 at 17:18, Sumit Kumar wrote: > Hi, > I want to know if there is a way to know if a variable is symbolic or not in > KLEE when KLEE is executing an instruction involving the variable. Within the application it self you can call ``klee_is_symbolic()``.

Re: [klee-dev] How to Interpret Klee Path Predicate

On 21 Mar 2016 10:33 a.m., "Azizul Hakim" wrote: > > How do we interpret the path predicates generated by KLEE. I've the following path predicates generated by S2E tool which uses KLEE. This predicate is generated from one branch of an IF-ELSE statement. > IIRC you're

Re: [klee-dev] how to clone an expression

On 24 March 2016 at 11:52, Sumit Kumar wrote: > Hi, > > Can anyone please tell me how to clone an expression. I want to get a copy > of given expression but they must not share any object. You are using the wrong mailing list.

Re: [klee-dev] KLEE generated only one path whereas program has two

> But the output from KLEE indicated that it completed only one path whereas > the program clearly has two paths. Can anyone please explain why this > happened ? Remember that KLEE executes LLVM IR, not C! You should look at the LLVM IR. If you look (see ``klee-last/assembly.ll``) you'll see that

Re: [klee-dev] Steps required for adding expr

Hi, On 4 April 2016 at 16:22, Sumit Kumar wrote: > Hi, > > I was reading Expr.h file when I came across this comment: > > Steps required for adding an expr: > -# Add case to printKind > -# Add to ExprVisitor > -# Add to IVC (implied value

Re: [klee-dev] How to Interpret Klee Path Predicate

On 4 April 2016 at 17:55, Azizul Hakim wrote: > Thanks Dan. I can also print the constraints in the format below. Do you > happen to have any idea where I can get a documentation of this format? > > > > (query [(Eq false > (Eq (w32 0x0) >

Re: [klee-dev] how to introduce a new symbolic variable

On 4 April 2016 at 15:34, Sumit Kumar wrote: > Hi, > > Can anyone please tell me how to introduce a new (not declared in test > program) symbolic variable from within KLEE. Your question is not specific enough. "symbolic variable" here could mean several different things.

Re: [klee-dev] how to add label to assert statements

Hi, On 29 April 2016 at 06:55, Sumit Kumar wrote: > Hi Dan, > > Thanks for introducing the z3 support. It has been great help. It has saved > me tons of work :). > Please find below my answers to some of your queries: > >>Yes your previous e-mails were misleading because

Re: [klee-dev] Some questions about SMT solvers

Hi Fabrizio, On 15 April 2016 at 13:10, Fabrizio Biondi wrote: > Hi all, > > I have been tinkering with KLEE's SMT solver chain, and I have a few > doubts some of you may find the time to address. > > 1) I have noticed that computeValidity returns 0 (Unknown) a lot.

Re: [klee-dev] Can klee generate a combined path expression to reach a particular statement?

Hi, On 27 January 2017 at 22:20, Cong Yan wrote: > Hi, > > Is klee able to generate an expression combining different paths? For > example, > > if (a) > stmt1; > else > stmt2; > stmt3; The answer is yes and no. It is all dependent on how the C program above is

Re: [klee-dev] One question about external dispatcher

On 27 January 2017 at 04:18, Qiuping Yi wrote: > Dear all, > > I encountered a strange problem when testing the next code snippet: > > 1 if (pw = getpwuid(getuid()) == NULL) > 2 return ; > > 3 .. = pw->pw_dir; Please use the correct mailing list (klee-dev@imperial.ac.uk)

[klee-dev] IMPORTANT: Build system changes

Hi All, For those using KLEE right now there are two important build system changes. ## Testing target names Testing target names have changed For the autoconf build system * the `check` target has been renamed `systemtests` * A new `check` target has been added that runs both the

Re: [klee-dev] klee-uclibc installation fails

On 17 August 2016 at 17:03, Reza Ahmadi wrote: > Hi, > > I had installed klee (with llvm 2.9) without klee-uclibc. Now I want to > re-install klee including klee-uclibc. When I try to configure it complains > that I need to install ncurses. > > I installed ncurses using this,

Re: [klee-dev] klee and c++14

Hi, On 15 August 2016 at 14:48, Leandro Rabindranath Leon wrote: > Hi > > Apologies if this is not the appropriate space for pose this question. > > As I have understood, I can not use klee on programs in C++14, as > llvm-3.4 does not support it. > > However, I would

Re: [klee-dev] Adding initial state as a constraint

Hi, On 2 March 2017 at 02:06, Chelsea Metcalf wrote: > > Hi, > > I am trying to add the initial state as a constraint, but it is not taking > effect. The above does not make sense to me. Please clarify your question. Perhaps with a code example to illustrate what you

Re: [klee-dev] segmentation fault

On 23 September 2016 at 23:43, Reza Ahmadi wrote: > Hi all, > > I tried to run a simple .cpp code using Klee. My code includes some > float-related operations. If I remove the float-related stuff, then, Klee is > successful in generating 3 test cases but fails if I include

Re: [klee-dev] Linking C++ runtime

On 26 September 2016 at 20:56, Eric Laberge wrote: > Hello! > > I am trying to get KLEE running a simple C++ app through Docker, but am > obviously not doing it correctly. Anybody got it working? > > Here’s what I got: > > klee@77c9c1d55f4a:/tmp$ cat hello.cpp > int main() {

Re: [klee-dev] Error in make check

On 18 September 2016 at 22:23, Awanish wrote: > Hi, > I configured klee with this command > ../configure --with-llvmsrc=/home/awanish/llvm-2.9/llvm-2.9 > --with-llvmobj=/home/awanish/llvm-2.9/llvm-2.9/build --with-stp=/usr/local > --with-uclibc=/home/awanish/klee-uclibc/

Re: [klee-dev] Cannot compile Coreutils 6.10 inside KLEE Docker image

On 11 November 2016 at 08:41, Thuan Pham wrote: > FYI, the same issue happens while configuring Coreutils-6.11. > > On Fri, Nov 11, 2016 at 4:33 PM, Thuan Pham wrote: >> >> Dear all, >> I am trying to reproduce results of KLEE OSDI'08 paper on

Re: [klee-dev] Adding support for another C library

Hi Marko On 16 October 2016 at 04:34, Marko Dimjašević wrote: > Hi again, > > On Fri, 2016-10-14 at 19:51 -0600, Marko Dimjašević wrote: > >> Earlier on this list there was a thread on what would be alternatives >> to >> KLEE-uClibc as the library implementation got rather

Re: [klee-dev] Adding support for another C library

On 17 October 2016 at 22:52, Marko Dimjašević <ma...@cs.utah.edu> wrote: > Hi Dan, > > On Mon, 2016-10-17 at 09:44 +0100, Dan Liew wrote: >> That is likely the cause error. This comes from a rather hacky >> implementation of a linker inside KLEE. >&

Re: [klee-dev] Testing newest Coreutils

On 24 November 2016 at 03:57, Thuan Pham wrote: > Hi, > Has anyone tried to use KLEE to test newest version of Coreutils, say 8.25? > I get stuck at the compilation step. Neither KLEE - LLVM2.9 nor KLEE - > LLVM3.4 can compile Coreutils successfully. > > Here is the error

Re: [klee-dev] Print out intermediate symbolic representation for each path instead on generating test-case for each path

Hi, On 2 November 2016 at 15:52, wrote: > Dear Klee developers, > > > I am trying to use Klee for specification generation. To do that I need > Klee's intermediate symbolic results. Specifically, I need the guards of > each path in the program to be printed in their

Re: [klee-dev] Path constraints as equations of integers

Hi, On 1 November 2016 at 12:17, Papapanagiotakis-Bousy, Iason wrote: > Hello, > > > > I am a new user of KLEE, I was looking into symbolic execution in order to > extract the constraints of the input variables of a program for each path in > the code.

Re: [klee-dev] Building constraints with Expr

Hi, > I am interested to build an Expr constraint given (in the simplest case) > something like “x == 0”, how would I do that? I presume that `x` refers to a symbolic variable here. KLEE's Expr language works on Arrays rather than plain variables so in order construct the expression you want

Re: [klee-dev] Is possible to mark a function as uninterpreted function?

Hi Javier, On 14 December 2016 at 13:28, Javier Godoy wrote: > Hi! > > Is possible to mark a function as uninterpreted function in Klee? > > Example i need: > > > foo(int a) > { > if( boo(a) > 0) > return 0; > else > return 1; > } > > boo(int x) //I want to

Re: [klee-dev] how to dampen ktest exuberance with symbolic index into symbolic array

Hi Richard, On 10 January 2017 at 00:19, Richard Rutledge wrote: > Consider the following program: > > //- > #include > #include > > #define BUFFER_SIZE 16 > > int main(int argc, char *argv[]) { > > char

Re: [klee-dev] Add a C++ file for klee's POSIX library

Hi, On 22 December 2016 at 05:37, Randall wrote: > Hello eyeryone. > > I have met a problem while adding a c++ library which uses > STL. So I get these error as follow: > > ... > > ... > > Unable to find size for global

Re: [klee-dev] find_llvm.cmake has problems in llvm version like 3.4svn

On 28 March 2017 at 14:51, 王悦 wrote: > Hi, all: > Recently, I was trying to compile KLEE with llvm-3.4. I came into a > problem that klee fail to recognize llvm version. When I looked into > find_llvm.cmake, I think I found the reason. > When try to match llvm version

Re: [klee-dev] LLVM directory does not exist/ not found

Hi, On 28 March 2017 at 13:50, Shaikha Al-Khuder wrote: > Hi there, > > I keep getting this type of error when trying to “make” within > klee_build_dir. > At first I tried trouble shooting through “sudo nano” each .h/.cpp file that > contains the non-existing file directory

Re: [klee-dev] KLEE "make" errors with LLVM-3.4.2

On 13 April 2017 at 13:11, Zhiyi Zhang wrote: > > Hi, > > I tried building KLEE on Ubuntu 16.04 LTS. I have built LLVM-3.4.2 (put Clang > into /llvm/tools,then cmake llvm )and STP-2.1.2. After I configured KLEE with > "cmake", > > cmake -DENABLE_SOLVER_STP=ON

Re: [klee-dev] Converting KQuery numbers to signed integers

Hi, On 7 April 2017 at 14:19, Papapanagiotakis-Bousy, Iason wrote: > Hello KLEE community, > > > > I was wondering how would I convert the numbers appearing in KQuery to > signed integers. > > Could you point me to the right direction on how to do that?

Re: [klee-dev] Using KLEE in LLVM Pass

Hi, On 19 July 2017 at 13:55, Khaled Yakdan wrote: > Hi, > > I am working on an LLVM analysis pass where I need to reason about whether > two values are equal. I am wondering if KLEE can be used for this purpose. > One idea would be to symbolically execute the given

Re: [klee-dev] klee and overshift error

On 22 July 2017 at 16:49, Andrew Santosa wrote: > Hi BNM, > > KLEE may report overshift error upon encountering Shl, AShr or LShr of LLVM. > It is reported when KLEE determines that the shift amount is greater than > the bitwidth of the data being > shifted. Slight

Re: [klee-dev] One phenomenon after the execution using klee

Hi, On 10 May 2017 at 03:55, 曾杰 wrote: > Hi, all, > If you write test.c with an error out of bound and test2.c with an > error assertion failed. > You first symbolically execution test.bc(using clang to generate), and > then the test2.c. you will find the contents

Re: [klee-dev] Current status of Z3 with FP-support

Hi, On 12 June 2017 at 13:12, Henrik Tjäder <hen...@tjaders.com> wrote: > Hi, > > Reading (1) and quoting Dan Liew, > > "I'm aware of klee-fp. However I should warn you (so that you don't > waste time doing this) that I (and another research institution) have > alr

Re: [klee-dev] KLEE on ASAN-enabled binaries

On 19 June 2017 at 15:48, Alexandre Adamski wrote: > Hello there, > > I was wondering: it is possible to use KLEE on a binary compiled with > AddressSanitizer? Obviously using WLLVM to get the LLVM IR. This won't work properly I'm afraid. When compiling with ASan a bunch

Re: [klee-dev] KLEE behaviour with function call to uclibc

Hi, On 28 May 2017 at 00:55, Shehbaz Jaffer wrote: > Hi Dan, > > > Thank you for your reply. However, I am struggling with how function not > defined in the programs bitcode (like getopt_long function) gets emulated by > KLEE. Please allow me to explain the steps

Re: [klee-dev] KLEE behaviour with function call to uclibc

On 27 May 2017 at 01:36, Shehbaz Jaffer wrote: > Hello KLEE developers, > > I am trying to understand how KLEE emulates environment variables. In > particular, how do functions like getopt_long get executed with KLEE, when we > give --sym-arg as an argument.

Re: [klee-dev] Getting path formula in dimacs format

Hi, On 11 June 2017 at 17:20, Awanish wrote: > Hi, > > I want to get/convert path constraint into dimacs/SAT format. Is there any > way to convert in the desired form? No such feature exists in KLEE itself but I think it should still be possible to get queries in the

Re: [klee-dev] failed external call: fgets

On 16 June 2017 at 17:05, Nourah mmm wrote: > Hi, > > I try to run KLEE on cutcp benchmark from (Parboil Benchmarks). The > benchmark consists from the following program: main.c parboil.c readatom.c > cutcpu.c excl.c output.c > > First I compile it with the following command:

Re: [klee-dev] Klee-uclibc.bca Error when Running Coreutils

On 7 May 2017 at 06:27, Zhiyi Zhang wrote: > Hi, > > > I have installed klee on Ubuntu(version, 14.04 64 bit) with LLVM-3.4,and I > successfully run the tutorial 1 & 2. However, I met a problem when I run > Coreutils 6.11. I used the same options which are showed on

Re: [klee-dev] Current status of Z3 with FP-support

Hi, On 12 June 2017 at 13:12, Henrik Tjäder <hen...@tjaders.com> wrote: > Hi, > > Reading (1) and quoting Dan Liew, > > "I'm aware of klee-fp. However I should warn you (so that you don't > waste time doing this) that I (and another research institution) have > alr

Re: [klee-dev] KLEE: ERROR: error loading program 'pallin.c': Invalid bitcode signature

On 12 October 2017 at 08:49, Chengyu Zhang wrote: > Maybe you should run KLEE on .bc file generated by Clang rather than .c > file. To add to that you can't use "Apple Clang". You need to use a version of Clang that uses the same version of LLVM that KLEE was built

Re: [klee-dev] Issue regarding pasting code in klee directory

On 11 September 2017 at 17:11, Mahinder.Shrivas wrote: > Hi, > > I am facing bit problem, I am not able to paste the code for maze example > (i.e. maze.c in Tutorial 3) in klee directory. I am trying to paste it in > example folder and then trying to run it through

Re: [klee-dev] Fwd: Request regarding downloading KLEE code

On 4 September 2017 at 11:20, Mahinder.Shrivas wrote: > Hi All, > > This is regarding KLEE code. I am trying to clone KLEE code through docker > by running this command (docker build -t klee/klee .) While doing that the > connection is getting refused. I tried many times

Re: [klee-dev] Missing floor, modf and pow

Hi, On 3 March 2018 at 07:29, Alberto Barbaro wrote: > Hi all, > few months ago I was trying to understand how to test pngpixel via KLEE and > after few suggestion I was able to do it. > > I have just one more question. When I run KLEE I have this output: > >