====================================================================== This file is part of the Yices SMT Solver. Copyright (C) 2017 SRI International. Yices is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. Yices is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with Yices. If not, see . ====================================================================== This file explains how to compile Yices on different platforms and how to build binary distributions (with or without GMP). CONTENT AND DIRECTORY STRUCTURE ------------------------------- The source subdirectories include ./src: source code for Yices proper ./tests: source code for test programs ./doc: documentation, notes ./utils: shell scripts and other utilities ./examples: example input files for testing ./etc: miscellaneous files that get added to the tar files The following subdirectories are created and used during compilation: ./configs: configuration files for each platform. Each file stores compilation options and other settings used by the Makefile(s). ./build: where all object, executable, and library files are built ./distribution: where the tar files are stored The 'build' subdirectory is organized by platform + compilation mode: The main compilation modes are 'release' and 'debug'. The default mode is 'release'. Less common compilation modes are available for profiling and help to debugging (cf. Makefile). The default compilation platform is whatever 'config.guess' returns, but some systems can have variant platforms (e.g., a 32bit build on a 64bit Linux system). Example: on an Intel Mac, there may be four subdirectories under build: ./build/i386-apple-darwin8.9.1-release (32bits/release) ./build/i386-apple-darwin8.9.1-debug (32bits/debug) ./build/x86_64-apple-darwin8.9.1-release (64bits/release) ./build/x86_64-apple-dawrin8.9.1-debug (64bits/debug) Each of these directories contains subdirectories for objects, libraries, and binaries. In a build mode, there are two variant compilations, namely, with or without GMP statically linked. This gives 6 different subdirectories for each pair platform/build mode. For example: ./build/i386-apple-darwin8.9.1-release/obj ./build/i386-apple-darwin8.9.1-release/lib ./build/i386-apple-darwin8.9.1-release/bin ./build/i386-apple-darwin8.9.1-release/static_obj ./build/i386-apple-darwin8.9.1-release/static_lib ./build/i386-apple-darwin8.9.1-release/static_bin These six directories are where the binaries/objects/library files are stored during compilation. When a binary distribution is built, the relevant files are first copied into one of the subdirectories: ./build/i386-apple-darwin8.9.1-release/dist ./build/i386-apple-darwin8.9.1-release/static_dist Then, the tarfiles are built from the content of the dist or static_dist directories. The tarfiles are then stored into ./distributions This is also where the source tarfile is stored if a source distribution is built. CONFIGURATION ------------- 1) Basics Configuration files are generated by './configure', and are kept separate for each platform. They are stored in the ./configs subdirectory, with a name of the form 'make.include.'. Each configuration file is derived from 'make.include.in' by the './configure' script. The rationale for this organization is to support parallel compilation on several machines from the same source directory (i.e., without having to run ./configure every time on each machine). Yices 1.0.xx does not allow this and that's a pain whenever we release a new version. The main 'Makefile' in the top-level directory determines the architecture and OS, and checks the compilation mode. The platform is determined from the architecture and OS and 'make' reads the configuration file for that platform. This sets several variables that are passed to a recursive make: ARCH= POSIXOS= YICES_TOP_DIR= YICES_MAKE_INCLUDE= YICES_MODE= YICES_VERSION=2.x.y MAJOR=2 MINOR=x PATCH_LEVEL=y To see how these variables are set, type 'make show-config' or 'make show-config MODE='. For example, on a linux/x86_64 platform, 'make show-config MODE=debug' gives ARCH is x86_64-unknown-linux-gnu POSIXOS is linux YICES_TOP_DIR is /homes/bruno/yices2 YICES_MAKE_INCLUDE is configs/make.include.x86_64-unknown-linux-gnu YICES_MODE is debug YICES_VERSION is 2.x.y More variables are set during configuration. For trouble-shooting, you can see the full list by typing 'make show-details' in the toplevel Yices directory. In most cases, these variables (CC, LD, etc.) are set to good default values, but the defaults may be overridden by giving options to the ./configure script. 2) Configuration options The usual options can be given to './configure' and the usual environment variables are taken into account (CC, CFLAGS, LD, LDFLAGS, CPPFLAGS, etc.). Type './configure --help' for details. 3) GMP library location There are Yices-specific options for dealing with GMP complications. Building Yices may require as many as three different GMP libraries: - dynamic library (e.g., /usr/local/lib/libgmp.so) - static library (e.g., /usr/local/lib/libgmp.a) - for some platforms, another version of libgmp.a compiled as position independent code may also be required. In addition, on Cygwin and Mingw, the static and dynamic GMP library require different header files 'gmp.h'. The ./configure script tries to locate these libraries and header files in default locations. If that fails, or if the defaults are wrong, the following options can be given to ./configure: --with-static-gmp= --with-static-gmp-include-dir= --with-pic-gmp= --with-pic-gmp-include-dir= NOTE: the --with-pic-gmp is useful only if your want to build a static Yices distribution and if libgmp.a is not position-independent by default. 4) Alternative platforms To set the platform to something else than the default, give option --build= or --host= to ./configure. This will store compilation flags for this platform in file './configs/make.include.'. Then this configuration file can be selected by giving an argument of the form 'OPTION=...' to the 'make' command. For example, the default platform for a Linux/64bit machine is 'x86_64-unknown-linux-gnu'. It may be possible to compile for 32bit on the same machine (depending on compiler and libraries). To configure for 32bit compilation, we build for the alternative platform 'i686-unknown-linux-gnu' This is done by first building a configuration file: ./configure --build=i686-unknown-linux-gnu CFLAGS=-m32 ... then selecting this configuration by typing make OPTION=32bits MAKEFILES --------- Three makefiles are involved during compilation. 1) The top-level 'Makefile' determines the configuration and compilation mode. It sets several variables that are passed to a recursive 'make' command. 2) The recursive 'make' uses 'Makefile.build'. This second makefile may create build directories and subdirectories and invoke another recursive 'make' command. 3) The last 'make' command will use the 'Makefile' located in the './src' or './tests/unit' directories. BUILD COMMANDS -------------- The build commands are of the form make 'OPTION=<...>' 'MODE=' The OPTION part can be used to select an alternative platform, if it's omitted, the default platform will be selected. The possible options are as follows: a) On systems that support both 32bit and 64bit builds OPTION=32bits select 32bit compilation OPTION=64bits select 64bit compilation b) on Cygwin, OPTION can be given to build for Windows native using the mingw compilers: OPTION=no-cygwin build for Windows/32bits OPTION=mingw32 OPTION=mingw64 build for Windows/64bits The possible modes are as follows: MODE=release (default mode: compile with optimization enabled) MODE=debug debug mode, no optimization MODE=devel same optimizations as release, compiled with assertions MODE=profile MODE=gcov MODE=valgrind MODE=quantify MODE=purify The last five modes select compilation flags to enable (or help) runtime analysis of the Yices executable using 'gprof', 'gcov', 'valgrind', etc. NOTE: for analysis with 'valgrind', it's usually sufficient to compile with 'MODE=debug'. MODE=valgrind is required in rare cases, when some bug manifests itself only when the code is compiled with optimizations. MODE=devel was added in September 2012. It is for development. In this mode, the same compilation flags are used as MODE=release. But MODE=devel enables use of modules for tracing/printing/debugging that are not part of the normal distribution. The main targets are: all build libraries + executables for the given platform binary-distribution build tarfile for a Yices binary distribution (this distribution is dynamically linked against GMP) static-distribution tarfile for a Yices static distribution (statically linked against GMP) source-distribution build a tarfile containing the Yices sources doc build the documentation Variants for the mingw distributions: dist prepare for a standard distribution (dynamically linked) static-dist prepare for a static distribution tarfile build a standard distribution tarfile (after dist + manual construction of lib file) static-tarfile build a static distribution tarfile (after static-dist + manual construction of lib file) Other possible targets: obj object files (for dynamic linking) static-obj object files (for static linking) lib libraries (dynamically linked against GMP) static-lib libraries (statically linked against GMP) bin executables (dynamically linked against GMP) static-bin executables (statically linked against GMP) test test programs (dynamically linked) static-test test programs (statically linked) sat sat solvers (dynamically linked) static-sat sat solvers (statically linked) install install libraries/executables/header files on the current machine show-config show some data about the configuration show-details show more data about the configuration check run the regression tests (in tests/regress) regress samt thing as 'check' For cleanup: clean remove everything in ./build/- arch-clean remove everything in ./build/-* all-clean remove everything in ./build/ and the generated files in ./src NOTES FOR LINUX BUILDS ---------------------- 1) Default build On most Linux distributions, GMP and gperf can be installed using a package management systems (e.g., 'apt-get' on Ubuntu). It's also straightforward to build and install them from the sources. The only issue may be that libgmp.a is not position-independent by default. So another version of GMP may have to be built. Check doc/GMP for help on building a position-independent 'libgmp.a'. Assuming GMP and gperf are in their default location, the following steps should work: ./configure --with-pic-gmp= make all make binary-distribution make static-distribution NOTES: 1) For increased portability, it's better to build Yices on an older distribution (e.g., Ubuntu 8.04). Newer distributions have new versions of glibc, which can introduce incompatibilities. Also, the versions we build on Linux 2.6 won't run on old Linux 2.4 kernels. 2) If there are several versions of libgmp.so and libgmp.a on the build machine, it's a good idea to set LDFLAGS and LD_LIBRARY_PATH correctly so that the right one is picked. If GMP is built with default options, it will install in /usr/local/lib, but there may be another version in /usr/lib (which is put there by apt-get install). In most cases, we want to use the GMP libraries in /usr/local/lib. To find a usable libgmp.a, the configure script first searches the directories that occur in LDFLAGS if any, then in LD_LIBRARY_PATH. So we must either have '/usr/local/lib' before '/usr/lib' in LD_LIBRARY_PATH, or set LDFLAGS correctly. Also when we link using -lgmp, we want to force the linker to find /usr/local/lib/libgmp.so first (rather than /usr/lib/libgmp.so). To achieve this, the simplest trick is to give LDFLAGS=-L/usr/local/lib as an option to the ./configure script. 2) Building for 32bits on a 64bit Linux machine It's possible to build 32bit code on a 64bit Linux machine. This depends on GCC and on whether the support 32bit libraries are present on the machine. On Ubuntu, these 32bit libraries can be installed using 'apt-get'. To build Yices for 32bit, the first step is to install GMP for 32bit (compiled from the source). Check doc/GMP for help. To force compilation in 32bit mode, add the flag -m32 to CFLAGS: ./configure --build=i686-unknown-linux-gnu CFLAGS=-m32 make all OPTION=32bits make binary-distribution OPTION=32bits make static-distribution OPTION=32bits NOTES: It may be necessary to give some options to the linker as follows: ./configure --build=i686-unknown-linux-gnu CFLAGS=-m32 LD='ld -melf_i386' It may also be necessary to use the --with-pic-gmp option. As before, LDFLAGS can be used to pick the right libgmp.so if there are several of them on the build machine. NOTES FOR MAC OS BUILDS ----------------------- The hardest part is usually to install GMP. Check doc/GMP for help. Also, it's a good idea to install GMP from the source (and install it in the default directory /usr/local/lib) rather than use Darwin port. Once GMP is installed, the build should work fine on any Mac OS X platform (including older powerpc hardware). It may also be required to install a newer version of autoconf than the one that comes by default on Mac OS (I haven't checked whether this is still true for newer versions of the OS). Compiling in 32bits and 64bits should work on Intel MACs that run Mac OS 10.5 or newer. However the default platform depends on the OS version: - on 10.5 (Leopard) the default is 32bit compilation the default platform is of the form i386-apple-darwin9.x.y (the x.y part varies with OS updates) - since 10.6 (Snow Leopard) the default is 64bit compilation default platform: x86_64-apple-darwin10.x.y There are also issues with having 32 and 64bit versions of GMP on the same machine. I normally use fat libraries, and a hack that allows me to have two copies of gmp.h (one for 32bits, one for 64bits). Check utils/gmp-hack.h for this. There are incompatibilities between the different OS versions so a version built on Mac OS 10.6 may not work on Mac OS 10.5 or older. To increase portability, it's a good idea to give option -mmacosx-version-min=10.5 to GCC. I don't know if we can go back more than that (i.e., -mmacosx-version-min=10.4)?. For compatibility with Mac OS 10.5, we may also need -isysroot /Developer/SDKs/MacOSX10.5.sdk but it doesn't seem to be required for Yices 2 (so far). Update: option -isysroot /Developer/SDKs/MacOSX10.5.sdk does not work out of the box, because the GMP header file is not found in /Developer/SDKs/MacOSX10.5.sdk. A work around is to add a symbolic link to /usr/local/include in /Developer/SDKs/MacOSX10.5.sdk/usr/local. The instructions below assume compilation on an Mac running Snow Leopard (i.e., Mac OS 10.6.8) and with GMP installed in /usr/local/lib. 1) Default build ./configure --with-pic-gmp= \ CFLAGS=-mmacosx-version-min=10.5 make all make binary-distribution make static-distribution 2) Build for 32bit on Mac OS X 10.6 ./configure --build=i386-apple-darwin10.8.0 \ --with-pic-gmp= \ CFLAGS='-m32 -mmacosx-version-min=10.5' make all OPTION=32bits make binary-distribution OPTION=32bits make static-distribution OPTION=32bits 3) Build for 64bits on Mac OS X 10.5 ./configure --build=x86_64-apple-darwin9.2.2 \ --with-pic-gmp=.... \ CFLAGS='-m64' make all OPTION=64bits make binary-distribution OPTION=64bits make static-distribution OPTION=64bits NOTES: on MacOS X Lion and newer versions, things may be a bit different: 1) Xcode 4.x for Lion no longer includes gcc as compiler. Instead, it includes some versions of llvm-gcc and clang. I tried using Xcode 4.1: the llvm-gcc that comes with it is buggy (it seg-faults while compiling Yices). The clang 2.1 distributed with Xcode 4.1 seems to work for compiling but it does not understand option -MG. Possible workaround: install llvm+clang 3.0 and use that. 2) Binaries and libraries are expected to all be position independent on MacOS X Lion and Mavericks. This causes some issues with GMP (at least with GMP 5.0.2). A solution is to build libgmp.a using position-independent flags (see the nodes in doc/GMP on how to do that). NOTES FOR CYGWIN AND MINGW BUILDS --------------------------------- It's somewhat more complicated to build Yices with both static and dynamic GMP libraries on Cygwin and Mingw than on other platforms. The issue is that GMP can't be installed in the standard place as both a static and a dynamic library. That's because each library uses a different 'gmp.h' include file (which is by default in /usr/include). A solution is to compile GMP twice from the source and install the dynamic and static libraries in different locations: 1) First, build GMP as a dynamic library in the default location. This can be done by giving options --enable-shared --disable-static when configuring GMP. This will build /usr/lib/libgmp.dll.a /usr/bin/cyggmp-3.dll The corresponding 'gmp.h' will be in /usr/include. 2) Build GMP as a static library in a different location (say /tools/static_gmp/). This can be done by giving options --disable-shared --enable-static --prefix=/tools/static_gmp to GMP's configure script. This will build /tools/static_gmp/lib/libgmp.a and the corresponding 'gmp.h' will be in /tools/static_gmp/include. After you've done that, you need to give special flags to the Yices's configure script so that it can find 'libgmp.a' in its nonstandard location and the corresponding 'gmp.h'. The best way to do this is to configure Yices using: ./configure --with-static-gmp=/tools/static_gmp/lib/libgmp.a \ --with-static-gmp-include-dir=/tools/static_gmp/include Then the build should work using the default commands: make all make binary-distribution make static-distribution NOTE: On both Cygwin and Mingw, the static 'libgmp.a' is position independent code so there's no need to specify a different PIC gmp. Option --with-pic-gmp should not be used on Cygwin or Mingw. NOTE: Possible compiler issue on Cygwin (noted 2010/11/16). On the cygwin version just installed on a Windows 7 machine, there are two gcc version (/usr/bin/gcc-3 and /usr/bin/gcc-4). The gcc-4 does not compile Yices in static mode (i.e., make static-bin fails). This seems to be due to the lack of libgcc_s.a on that installation. Don't know what this library is about. Possible fixes: 1) Force compilation with gcc-3: give CC=/usr/bin/gcc-3 to the ./configure script 2) Add option -static-libgcc when building in static mode (cf. src/Makefile) BUILDING A WINDOWS 32bit VERSION FROM CYGWIN -------------------------------------------- On Cygwin, the default compilation produces code that requires Cygwin libraries at run time. This code cannot run on a native Windows machine that does not have Cygwin installed. To build a version of Yices that can run on a native Windows machine, you can either install Mingw and msys and compile from there, or compile from Cygwin using --build=i686-pc-mingw32 to select a Mingw32 configuration. For the result to work, you must either give the flag -mno-cygwin to GCC or use a cross compiler. Using -mno-cygwin is easier but may no longer be supported by new versions of GCC. OLD METHOD: Using the -mno-cygwin flag To do this, type ./configure --build=i686-pc-mingw32 CFLAGS=-mno-cygwin This will produce configuration file 'make.include.i686-pc-mingw32' in directory ./configs. To use this configuration file rather than the default, add OPTION=no-cywgin when invoking make. For example, make all OPTION=no-cygwin The result will be in ./build/i686-pc-mingw32-release/ You need to have a version of GMP compiled for mingw32 for this to work. The path to that library can be given using --with-static-gmp, etc. or by giving options LDPATH=... CPPFLAGS=... to ./configure MEW METHOD: Using a cross compiler 1) Get the cross compiler: start 'setup.exe' in Windows then install the packages 'mingw64-i686-gcc' and relatives. The cross compiler is /usr/bin/i686-w64-mingw32-gcc 2) Build and install a 32bit version of GMP using the cross compiler (read doc/GMP). Two versions of GMP must be installed. On my machine, the dynamic GMP library was built with --prefix=/home/bruno/tools/mingw32 and the static version was built with --prefix=/home/bruno/tools/mingw32/static 3) Configure yices as follows: ./configure --build=i686-pc-mingw32 \ CC=/usr/bin/i686-w64-mingw32-gcc \ LD=/usr/bin/i686-w64-mingw32-ld \ STRIP=/usr/bin/i686-w64-mingw32-strip \ RANLIB=/usr/bin/i686-w64-mingw32-ranlib \ CPPFLAGS=-I/home/bruno/tools/mingw32/include \ LDFLAGS=-L/home/bruno/tools/mingw32/lib \ --with-static-gmp=/home/bruno/tools/mingw32/static/lib/libgmp.a \ --with-static-gmp-include-dir=/home/bruno/tools/mingw32/static/include 3a) Aternative method: use --host=i686-w64-ming32 when running ./configure ./configure --host=i686-w64-mingw32 \ CPPFLAGS=-I/home/bruno/tools/mingw32/include \ LDFLAGS=-L/home/bruno/tools/mingw32/lib \ --with-static-gmp=/home/bruno/tools/mingw32/static/lib/libgmp.a \ --with-static-gmp-include-dir=/home/bruno/tools/mingw32/static/include 4) Compile using OPTION=mingw32 (or OPTION=no-cygwin) make all OPTION=mingw32 make dist OPTION=mingw32 make static-dist OPTION=mingw32 5) Build the library files 'liyices.lib' by hand (using the Visual Studio 'lib' tool) See the notes below for help on how to do this. 6) Build the tar files make tarfile OPTION=mingw32 make static-tarfile OPTION=mingw32 BUILDING A WINDOWS 64bit VERSION FROM CYGWIN ---------------------------------------------- This can be done using the mingw64 cross compiler on Cygwin. 1) To get the cross compiler, start the setup.exe utility in Windows. Then install the packages mingw64-x86_64-gcc and relatives. These are in section 'devel' of 'setup.exe' The mingw64 compiler is installed as /usr/bin/x86_64-w64-mingw32-gcc 2) Build and install a 64bit version of GMP. Read doc/GMP for help. There should be two versions of GMP/64bits installed for Yices to configure properly. On my Dell laptop: the dynamic GMP/64bits library was installed with --prefix=/home/bruno/tools/mingw64 The static GMP/64bits library was installed with --prefix=/home/bruno/tools/mingw64/static So this means that we have the following files: /home/bruno/tools/mingw64/bin/libgmp-10.dll (GMP DLL) /home/bruno/tools/mingw64/lib/libgmp.dll.a (corresponding lib file) /home/bruno/tools/mingw64/include/gmp.h (corresponding include) /home/bruno/tools/mingw64/static/lib/libgmp.a (static GMP) /home/bruno/tools/mingw64/static/include/gmp.h (corresponding include) 3) Assuming this installation, configure Yices as follows ,/configure --host=x86_64-w64-mingw32 \ CPPFLAGS=-I/home/bruno/tools/mingw64/include \ LDFLAGS=-L/home/bruno/tools/mingw64/lib \ --with-static-gmp=/home/bruno/tools/mingw64/static/lib/libgmp.a \ --with-static-gmp-include-dir=/home/bruno/tools/mingw64/static/include or like this ./configure --build=x86_64-pc-mingw32 \ CC=/usr/bin/x86_64-w64-mingw32-gcc \ LD=/usr/bin/x86_64-w64-mingw32-ld \ STRIP=/usr/bin/x86_64-w64-mingw32-strip \ RANLIB=/usr/bin/x86_64-w64-mingw32-ranlib \ CPPFLAGS=-I/home/bruno/tools/mingw64/include \ LDFLAGS=-L/home/bruno/tools/mingw64/lib \ --with-static-gmp=/home/bruno/tools/mingw64/static/lib/libgmp.a \ --with-static-gmp-include-dir=/home/bruno/tools/mingw64/static/include To select this configuration give 'OPTION=mingw64' to the make commands. FOR WINDOWS/MINGW DISTRIBUTIONS: MANUAL STEPS TO BUILD libyices.lib ------------------------------------------------------------------- This must be done when building the mingw32 or mingw64 distributions (after make dist or make static-dist, and before make tarfile or make static-tarfile). This requires Visual Studio to be installed on the machine (the free version, Visual Studio Express is good enough for this). For a 32bit Windows distribution (mingw32): 1) Open a Visual studio C++ command prompt (in Windows) 2) Go to the directory dist/lib or static_dist/lib directory for Yices/mingw32: c:\cygwin\home\...\build\i686-pc-mingw32-release\dist\lib or c:\cygwin\home\...\build\i686-pc-mingw32-release\static_dist\lib These directories should contain: libyices.a libyices.dll.a libyices.dll libyices.def 3) From the Visual studio prompt, type lib /def:libyices.def /machine:x86 This will create libyices.lib and libyices.exp 4) Cleanup: delete libyices.def and libyices.exp (they are not needed). 5) Build the tarfile. For 64bit Windows distribution (mingw64): The libraries are in c:\cygwin\home\...\build\x86_64-pc-mingw32\dist\lib and c:\cygwin\home\...\build\x86_64-pc-mingw32\static_dist\lib The procedure is the same as for mingww32, except in step 3. To create a lib file for 64bit Windows (x86_64 hardware), use: lib /def:libyices.def /machine:x64 NOTE: It's also possible to call the Visual Studio 'lib' utility directly from Cygwin, provided the executable and the DLL(s) it requires are in the PATH. The Yices source contains a shell script './utils/setup-vs2010' that does it for my Windows machine. This script must probably be adjusted depending on the Visual Studio Version and location. It must be run from a Cygwin shell (bash) using source ./utils/setup-vs1010 NOTE: (Updated 2011/12/01). There's a shell script in ./utils that makes it easier to build the Windows 32/64 bits distributions from cygwin. GCC GIVES WARNINGS ABOUT INLINED FUNCTIONS ------------------------------------------ Compiling yices with gcc-4.4 with the default options causes a lot of warnings of the form: warning: inlining failed in call to 'xxx': call is unlikely and code size would grow The yices functions that are declared 'inline' are small and do not cause much code growth. So these warnings are annoying. Similar warnings are produced by other versions of GCC too (e.g., GCC-4.5.3 for mingw32 and mingw64). The warnings are caused by heuristics that GCC employs to determine whether it is worth inlining a function call. GCC attempts to determine whether a basic block is executed frequently enough before inlining the function calls in that block. By default, GCC uses crude heuristics to guess the execution frequency of each block (and other heuristics to estimate code growth). The part about 'code size would grow' can be misleading. The warning will be produced even if inlining does not cause any code growth at all, probably because the code-growth estimate is not very accurate. The preferred way to fix this is to add option -fno-guess-branch-probability to CFLAGS when configuring Yices: ./configure CFLAGS=-fno-guess-branch-probability Other ways to prevent these warnings: 1) remove -Winline from the compilation flags in src/Makefile. GCC will inline whatever it wants and there will be no warnings. 2) add __attribute__ ((always_inline)) to the inline functions that cause problem. GCC will stop checking whether the size grows and whether the call is likely. 3) play with the parameters that control what GCC considers high enough frequency (e.g., add option --param hot-bb-frequency-fraction=2000)