search for: seahorn

Hi folks, We would like to add SeaHorn <http://seahorn.github.io/> and Crab-llvm <https://github.com/seahorn/crab-llvm> to the list of LLVM's users on http://llvm.org/Users.html under Open Source Projects. The descriptions would be: 1. SeaHorn | An Algorithmic Logic-Based Reasoning Framework. 2. Crab-llvm | A static ana...

Hello, I am on the hook to instrument a piece of legacy LLVM IR code, and then we are planning to feed to the SeaHorn framework for some model checking tasks. After the instrumentation, I tried to use llc (version 3.9) to compile the IR code, and it works fine. However, when I try to use llc (version 3.8.1, the default llvm version of SeaHorn) to compile the IR code, it shows the following error: LLVM ERROR: Uns...

Hi, I'm looking for interprocedural AAs and have, of course, found https://llvm.org/docs/AliasAnalysis.html. However, the AAs that come bundled with LLVM do not work interprocedurally in a way that I need it (on/with stack variables). The two interesting looking AAs come with the optional `poolalloc' module that hasn't been updated in years (I guess

...ure why you are concerned about memcpy and bitcasts, but if you call MCpyInst->getSource() and MCpyInst->getDest() it will look through casts and give you the 'true' source/destination. If you want to get rid of memcpy altogether, you can take a look at this pass: https://github.com/seahorn/seahorn/blob/master/lib/Transforms/Scalar/PromoteMemcpy.cc . Best, Kuba On Tue, Jan 30, 2018 at 3:22 AM, ma jun via llvm-dev < llvm-dev at lists.llvm.org> wrote: > Hi Craig > Thank you very much ！ > > 2018-01-30 16:11 GMT+08:00 Craig Topper <craig.topper at gmail.com>...

Hello List, I am on the hook to instrument a piece of legacy LLVM IR code, and then we are planning to feed to the SeaHorn framework for some model checking tasks. After the instrumentation, I tried to use llc (version 3.9) to compile the IR code, and it works fine. However, when I try to use llc (version 3.8.1, the default llvm version of SeaHorn) to compile the IR code, it shows the following error: LLVM ERROR: Uns...

Hi Alberto, I have not used this myself, but I think you should be able to visit your Instruction ‘users()’. I think the name this function was given is a bit confusing, but this returns an iterator range you can iterate through to find instructions that depend on a given one. Similarly, you have the function ‘uses()’ that can be used to traverse down the DAG when instructions are still on SSA

On 31 Jan 2018, at 17:36, Jakub (Kuba) Kuderski via llvm-dev <llvm-dev at lists.llvm.org> wrote: > > If you want to get rid of memcpy altogether, you can take a look at this pass: https://github.com/seahorn/seahorn/blob/master/lib/Transforms/Scalar/PromoteMemcpy.cc . There are at least four different places in LLVM where memcpy intrinsics are expanded to either sequences of instructions or calls: - InstCombine does it for very small memcpys (with a broken heuristic). - PromoteMemCpy does it mostly...

Dear Developers, I am a Master's student at the ECE department of the University of Florida, USA.​​ For my research project, supervised by Prof. Mark Tehranipoor<http://tehranipoor.ece.ufl.edu/> and Prof. Farimah Farahmandi<http://farimah.ece.ufl.edu/>, I need to use Clang LLVM DataflowSanitizer library in KLEE. However, I have faced some difficulties (explained below) while

Hi Craig Thank you very much ！ 2018-01-30 16:11 GMT+08:00 Craig Topper <craig.topper at gmail.com>: > The pointers must always be i8* the alignment is independent and is > controlled by the attributes on the arguments in the call to memcpy. > > ~Craig > > On Mon, Jan 29, 2018 at 11:45 PM, ma jun <jun.parser at gmail.com> wrote: > >> Hi >> >>

.../llvm/ADT/STLExtras.h:139:13: error: no type named 'type' in 'std::__1::result_of<std::__1::pointer_to_unary_function<llvm::DSNode *, llvm::DSNode &> (llvm::DSNode &)>' ::type value_type; ~~^~~~ /Users/jaredcarlson/Projects/crab-llvm/dsa-seahorn/include/dsa/DSGraphTraits.h:122:25: note: in instantiation of template class 'llvm::mapped_iterator<llvm::ilist_iterator<llvm::ilist_detail::node_options<llvm::DSNode, true, false, void>, false, false>, std::__1::pointer_to_unary_function<llvm::DSNode *, llvm::DSNode &am...

The pointers must always be i8* the alignment is independent and is controlled by the attributes on the arguments in the call to memcpy. ~Craig On Mon, Jan 29, 2018 at 11:45 PM, ma jun <jun.parser at gmail.com> wrote: > Hi > > > 2018-01-30 15:36 GMT+08:00 ma jun <jun.parser at gmail.com>: > >> Hi >> Thanks ! >> so for this example >>