search for: z3prover

...solver [1]. Much of what I'm going to say is covered in [2] which is a bug report I opened (including a heap-use-after-free AddressSanitizer finds, I'm not sure if this a false positive or not) but here are the basics of what I found. Build Z3 as follows ``` git clone https://github.com/Z3Prover/z3.git cd z3 # Now apply the attached patch. # Basically this makes it so that in ``examples/c/test_capi.c`` # the main() function only calls two functions. # Note if you build without the patch when running ``c_example`` program AddressSanitizer # reports a heap-use-after-free. I'm not sure i...

Hi Chris, Thanks for answering, Can u clarify on this comment mentioned in https://github.com/Z3Prover/z3/issues/861 . cplusplus no exception support · Issue #861 · Z3Prover/z3 · GitHub - LLVM's *source code* does not use exceptions for performance reasons and so is compiled by default with -fno-exceptions. When using LLVM's libraries via it's C++ interface it is important t...

...mpiling C++ code that uses exceptions. Does this answer your question? -Chris > On May 1, 2018, at 10:38 AM, Siddharth Shankar Swain <h2015096 at pilani.bits-pilani.ac.in> wrote: > > Hi Chris, > Thanks for answering, Can u clarify on this comment mentioned in https://github.com/Z3Prover/z3/issues/861 <https://github.com/Z3Prover/z3/issues/861> . > > cplusplus no exception support · Issue #861 · Z3Prover/z3 · GitHub > LLVM's source code does not use exceptions for performance reasons and so is compiled by default with -fno-exceptions. When using LLVM's lib...

Siddharth, I'm not sure what coding standards you refer to when you say "some C++ coding standard". This question is answered in the LLVM Coding Standards document here: https://www.llvm.org/docs/CodingStandards.html#do-not-use-rtti-or-exceptions <https://www.llvm.org/docs/CodingStandards.html#do-not-use-rtti-or-exceptions> As such LLVM's coding standards prohibit the

Hi all, Can anyone explain why exceptions are disabled in LLVM, even if some C++ coding standard tells to use exceptions ? Thanks, Siddharth -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20180501/ed7903db/attachment-0001.html>

...;> relying on memory layout, etc.). I'm also observing ASan reporting a >> heap-use-after-free which Valgrind is not reporting, which makes me >> wonder if it is a false positive. > > > Let us start from this heap-use-after-free report. The one in > https://github.com/Z3Prover/z3/issues/436 looks legitimate. > Unless the application does something extremely weird and tricky, > heap-use-after-free reports are usually true positives. The developers tell me they are doing some unusual things and they believe that this might the cause of the report. > Can you some...

...eption in LLVM > Message-ID: > <CAMkbrzKtMUrYVSA_Ke3YJA=jkZNms1N9Ao9_2DWVfwD3qcqn8g at mail. > gmail.com> > Content-Type: text/plain; charset="utf-8" > > Hi Chris, > Thanks for answering, Can u clarify on this comment mentioned in > https://github.com/Z3Prover/z3/issues/861 . > > cplusplus no exception support · Issue #861 · Z3Prover/z3 · GitHub > > - LLVM's *source code* does not use exceptions for performance reasons > and so is compiled by default with -fno-exceptions. When using LLVM's > libraries via it's C++...

On 11 February 2016 at 17:08, Reid Kleckner <rnk at google.com> wrote: > On Thu, Feb 11, 2016 at 5:53 AM, Dan Liew via cfe-dev > <cfe-dev at lists.llvm.org> wrote: >> >> > Can you somehow verify that this heap-use-after-free is happening? >> > E.g. print all the pointer values coming from memory::allocate, coming >> > into >> >