Re: [klee-dev] LLVM Error in Klee: does not support intrinsic function
Hi Cristian, Sure will report as an issue on github Thanks! On Tue, Jun 12, 2018 at 8:57 PM Cristian Cadar wrote: > Thanks for reporting this. Can you create a small test case and fill > out a bug report on GitHub? > > Cristian > > On 11/06/18 05:20, Ridwan Shariffdeen wrote: > > Hi, > > > > I am trying to run klee with OpenJPEG > > (https://github.com/uclouvain/openjpeg), and encountered the following > > error: > > > > LLVM ERROR: Code generator does not support intrinsic function > > 'llvm.x86.sse2.psrai.d'! > > > > Is it some limitation in Klee with vector generation > > (https://github.com/klee/klee/issues/660) ? or am I missing some > > instruction? > > > > I am using WLLVM to compile with debug info and using extract-bc to > > generate the bytecode. > > > > Any help on this is appreciated. > > > > Thanks! > > > > > > > > ___ > > klee-dev mailing list > > klee-dev@imperial.ac.uk > > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > > > ___ > klee-dev mailing list > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Options for symbolic environments no longer exist?
This should still work under Docker. Are you sure you are passing the options correctly? Those are not options to the KLEE tool itself, take a look at the tutorials for examples. If you still have problems, please fill out a bug report detailing the exact steps you followed. Cristian On 09/06/18 22:36, Sang Phan wrote: Hello, I want to use KLEE with symbolic file or stdin. According to the following document, I need to use -sym-files or -sym-stdin http://klee.github.io/docs/options/ However, these options no longer exist in the latest release of KLEE (docker). May I ask if they are broken, or are changed to something else? Thank you, Sang ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] LLVM Error in Klee: does not support intrinsic function
Thanks for reporting this. Can you create a small test case and fill out a bug report on GitHub? Cristian On 11/06/18 05:20, Ridwan Shariffdeen wrote: Hi, I am trying to run klee with OpenJPEG (https://github.com/uclouvain/openjpeg), and encountered the following error: LLVM ERROR: Code generator does not support intrinsic function 'llvm.x86.sse2.psrai.d'! Is it some limitation in Klee with vector generation (https://github.com/klee/klee/issues/660) ? or am I missing some instruction? I am using WLLVM to compile with debug info and using extract-bc to generate the bytecode. Any help on this is appreciated. Thanks! ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
