similar to: Question about Formal Verification

I'd just like to thank everyone who replied on this; the suggestions and resources are very helpful! ~Scott On Tue, Feb 9, 2016 at 8:38 PM, Andrew Santosa <santosa_1999 at yahoo.com> wrote: > LLBMC http://llbmc.org uses bounded model checking technique to find > errors in LLVM IR. > Model checking is essentially search, and since LLBMC is bounded, the > search for errors

LLBMC http://llbmc.org uses bounded model checking technique to find errors in LLVM IR.Model checking is essentially search, and since LLBMC is bounded, the search for errors is usuallyincomplete, hence the approach may not verify the entire program, however, it may be goodenough to find interesting errors. Best wishes,Andrew On Monday, 8 February 2016, 21:54, Scott Santucci via llvm-dev

LLVM_DEFINITIONS used to be defined as set(LLVM_DEFINITIONS "-D__STDC_LIMIT_MACROS" "-D__STDC_CONSTANT_MACROS") Now it is defined as set(LLVM_DEFINITIONS " -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS") (note that it is no longer a cmake list but a string, and the string contains a leading space!) This causes CMake 3.1 to emit g++ -D

I am currently setting up my Module with module->setTargetTriple(llvm::sys::getProcessTriple() #ifdef _WIN32 + "-elf" #endif ); And my ExecutionEngine with llvm::EngineBuilder(std::move(module)) .setErrorStr(&err) .setMCPU(llvm::sys::getHostCPUName())

I made this change (not specifically changing from a list to a string, but changing from a hardcoded value to the value that was actually decided by cmake), and I checked that it works with cmake 2.8.12.2 which is the minimum version set in CMakeLists.txt. So if it doesn’t work with cmake 3.1/3.2 then that looks like something new that was introduced after 2.8.12.2. I’ll have a look at this

I encountered a new build failure (r227128) on my nightly build of LLVM for MinGW: FAILED: cmd.exe /c cd . && D:\MinGW\x86_64-4.9.1-release-posix-seh-rt_v3-rev0\mingw64\bin\c++.exe -Wall -W -Wno-unused-parameter -Wwrite-strings -Wcast-qual -Wno-missing-field-initializers -pedantic -Wno-long-long -Wno-maybe-uninitialized -Wno-comment -std=gnu++11 -g

On Tue, Jan 27, 2015 at 10:02 AM, Mueller-Roemer, Johannes Sebastian <Johannes.Sebastian.Mueller-Roemer at igd.fraunhofer.de> wrote: > Adding -D__MSVCRT_VERSION__=0x900 (or higher) to CMAKE_CXX_FLAGS and > -lmsvcr90 (or higher) to CMAKE_CXX_STANDARD_LIBRARIES appears to work. > -lmsvcrt80 does not work, contrary to the comment on the MinGW bug tracker. > However, if you do not

Both Release and $CONFIG tblgen are built but the Release one is always used. At least with Visual C++ the Release tblgen is much faster than the Debug one. 2015-05-29 9:37 GMT+03:00 Mueller-Roemer, Johannes Sebastian < Johannes.Sebastian.Mueller-Roemer at igd.fraunhofer.de>: > Do they really allways put them into Release/bin or rather $<CONFIG>/bin? > > > > -- >

Yes, that's the idea, when you -DLLVM_OPTIMIZED_TABLEGEN=ON tblgen is built in Release in addition to whatever /property:Configuration= is. 2015-05-29 10:03 GMT+03:00 Mueller-Roemer, Johannes Sebastian < Johannes.Sebastian.Mueller-Roemer at igd.fraunhofer.de>: > That it’s faster is no surprise. Is the Release tblgen even built when > you build in Debug mode? Otherwise this

Indeed, mingw and pthreads have C++11 atomics, so building clang (with atomics) should be possible even in cross compilation. I have no idea what is the win from *not* using winpthreads, it is one small DLL file with BSD license. For context (does not matter to mingw as host for buiilding clang but matters for clang running with mingw environment), clang TLS implementation is not same as mingw so

I noticed that runFunction (for MCJIT) is very limited. At the same time the interpreter already has a fairly generic way of calling functions from a pointer and a Function * (for description) using libffi. Would it make sense to pull that functionality out into a small support library and using it in MCJIT? As is runFunction isn't particularly usable. -- Johannes S. Mueller-Roemer, MSc Wiss.

Hi Chris and everyone else, I just noticed that some of my builds broke due to commit 280013, as LLVM_INCLUDE_DIRS was renamed to LLVM_INCLUDE_DIR. In and of itself, not much of an issue as the fix is just to remove one character (in a couple of places). However, I would like to discuss if this rename is desirable at all. Sure, in-tree LLVM_INCLUDE_DIR is used everywhere, however not providing an

On 17 September 2014 13:27, Mueller-Roemer, Johannes Sebastian <Johannes.Sebastian.Mueller-Roemer at igd.fraunhofer.de> wrote: > Yes, this is incredibly annoying, so please avoid that. However I noticed that the current solution using CMake is broken, as I cannot enter my own ZLIB_ROOT, since no proper find_package is used. I just had a go at hacking this so that we use

On 17 September 2014 15:47, Mueller-Roemer, Johannes Sebastian <Johannes.Sebastian.Mueller-Roemer at igd.fraunhofer.de> wrote: > It's half the way there. Configuring and compiling works, but linking fails, probably some definition mismatches... It configured, compiled and linked okay for me. Could you look into it? > > But it can definitely be simplified, as due to the

The new patch works fine, but considering the discussion on the CMake bug tracker, I'm would say that TO_NATIVE_PATH shouldn't be used at all. ________________________________________ From: Dan Liew [dan at su-root.co.uk] Sent: Wednesday, July 23, 2014 10:38 AM To: Mueller-Roemer, Johannes Sebastian Cc: llvmdev at cs.uiuc.edu Subject: Re: [LLVMdev] [patch] EXPORTED_SYMBOL_FILE using mingw

That it’s faster is no surprise. Is the Release tblgen even built when you build in Debug mode? Otherwise this introduces the need to build Release before Debug. -- Johannes S. Mueller-Roemer, MSc Wiss. Mitarbeiter - Interactive Engineering Technologies (IET) Fraunhofer-Institut für Graphische Datenverarbeitung IGD Fraunhoferstr. 5 | 64283 Darmstadt | Germany Tel +49 6151 155-606 | Fax +49

On 17 September 2014 16:34, Mueller-Roemer, Johannes Sebastian <Johannes.Sebastian.Mueller-Roemer at igd.fraunhofer.de> wrote: > I'll have another look tomorrow. Thanks. > IMO, it is unnecessary clutter. It will fail if ${ZLIB_LIBRARIES} or ${ZLIB_INCLUDE_DIRS} are used anyways as they will be set to NOTFOUND. Or we go back to a silent-fail solution: Fair enough. I've never

This is a problem with all floating point folding, not just with these operations. What Matt is proposing is consistent with how we fold other libm intrinsics. —Owen > On Aug 18, 2014, at 1:22 AM, Mueller-Roemer, Johannes Sebastian <Johannes.Sebastian.Mueller-Roemer at igd.fraunhofer.de> wrote: > > Wouldn’t it be better to use the target’s implementation (if there is one)

I noticed some odd behavior with APFloat's convertFromString method. 1. If I pass the hex representation of the closest value to 0.1 (0x19999Ap-24), everything is fine and opOk is returned. However, if I pass the same value as a decimal string (0.10000002384185791015625), opInexact is set. 2. On the lower end of the scale, the smallest denormal 0x1p-149 returns opOk, but the

On Wed, Sep 17, 2014 at 12:27:42PM +0300, Yaron Keren wrote: > Large software libraries like OpenCV (under 3rdparty directory) do include > copies of zlib and friends and build it, for that reasons. The source code > is just half a megabyte and I think the license is compatible. We could do > the same with zlib or miniz. >From a packager's perspective, library bundling is one