Thanks for using Compiler Explorer
Sponsors
C++
LLVM IR
Cppx
Cppx-Gold
Cppx-Blue
C
Rust
D
Go
ispc
Haskell
OCaml
Python
Swift
Pascal
Fortran
Assembly
Analysis
CUDA
Zig
Clean
Ada
Nim
c source #1
Output
Compile to binary
Run the compiled output
Intel asm syntax
Demangle identifiers
Filters
Unused labels
Library functions
Directives
Comments
Horizontal whitespace
Compiler
6502 cc65 2.17
6502 cc65 2.18
6502 cc65 2.19
6502 cc65 trunk
ARM gcc 10.2 (linux)
ARM gcc 10.2.1 (none)
ARM gcc 10.3 (linux)
ARM gcc 4.5.4 (linux)
ARM gcc 4.6.4 (linux)
ARM gcc 5.4 (linux)
ARM gcc 5.4.1 (none)
ARM gcc 6.3.0 (linux)
ARM gcc 6.4 (linux)
ARM gcc 7.2.1 (none)
ARM gcc 7.3 (linux)
ARM gcc 8.2 (WinCE)
ARM gcc 8.2 (linux)
ARM gcc 8.3.1 (none)
ARM gcc 9.2.1 (none)
ARM gcc 9.3 (linux)
ARM gcc trunk (linux)
ARM msvc v19.0 (WINE)
ARM msvc v19.10 (WINE)
ARM msvc v19.14 (WINE)
ARM64 gcc 10.2
ARM64 gcc 10.3
ARM64 gcc 5.4
ARM64 gcc 6.3
ARM64 gcc 6.4
ARM64 gcc 7.3
ARM64 gcc 8.2
ARM64 gcc 9.3
ARM64 gcc trunk
ARM64 msvc v19.14 (WINE)
AVR gcc 4.5.4
AVR gcc 4.6.4
AVR gcc 5.4.0
Arduino Mega (1.8.9)
Arduino Uno (1.8.9)
FRC 2019
FRC 2020
K1C gcc 7.4
K1C gcc 7.5
KVX gcc 7.5 (ACB 4.1.0)
KVX gcc 7.5 (ACB 4.1.0-cd1)
KVX gcc 7.5 (ACB 4.2.0)
KVX gcc 7.5 (ACB 4.3.0)
KVX gcc 7.5 (ACB 4.4.0)
MIPS gcc 5.4
MIPS gcc 5.4 (el)
MIPS64 gcc 5.4
MIPS64 gcc 5.4 (el)
MSP430 gcc 4.5.3
MSP430 gcc 5.3.0
MSP430 gcc 6.2.1
PowerPC gcc 4.8.5
PowerPC64 gcc 6.3.0
RISC-V rv32gc clang (trunk)
RISC-V rv32gc clang 10.0.0
RISC-V rv32gc clang 10.0.1
RISC-V rv32gc clang 11.0.0
RISC-V rv32gc clang 11.0.1
RISC-V rv32gc clang 9.0.0
RISC-V rv32gc clang 9.0.1
RISC-V rv32gc gcc 10.2.0
RISC-V rv32gc gcc 8.2.0
RISC-V rv64gc clang (trunk)
RISC-V rv64gc clang 10.0.0
RISC-V rv64gc clang 10.0.1
RISC-V rv64gc clang 11.0.0
RISC-V rv64gc clang 11.0.1
RISC-V rv64gc clang 9.0.0
RISC-V rv64gc clang 9.0.1
RISC-V rv64gc gcc 10.2.0
RISC-V rv64gc gcc 8.2.0
Raspbian Buster
Raspbian Stretch
SDCC 4.0.0
TCC (trunk)
TCC 0.9.27
armv7-a clang (trunk)
armv7-a clang 10.0.0
armv7-a clang 10.0.1
armv7-a clang 11.0.0
armv7-a clang 11.0.1
armv7-a clang 9.0.0
armv7-a clang 9.0.1
armv8-a clang (trunk)
armv8-a clang (trunk, all architectural features)
armv8-a clang 10.0.0
armv8-a clang 10.0.1
armv8-a clang 11.0.0
armv8-a clang 11.0.1
armv8-a clang 9.0.0
armv8-a clang 9.0.1
power64 AT12.0 (gcc8)
power64 AT13.0 (gcc9)
power64le AT12.0 (gcc8)
power64le AT13.0 (gcc9)
power64le clang (trunk)
powerpc64 clang (trunk)
x64 msvc v19.0 (WINE)
x64 msvc v19.10 (WINE)
x64 msvc v19.14 (WINE)
x86 gcc 1.27
x86 msvc v19.0 (WINE)
x86 msvc v19.10 (WINE)
x86 msvc v19.14 (WINE)
x86 tendra (trunk)
x86-64 clang (assertions trunk)
x86-64 clang (trunk)
x86-64 clang 10.0.0
x86-64 clang 10.0.1
x86-64 clang 11.0.0
x86-64 clang 11.0.1
x86-64 clang 12.0.0
x86-64 clang 3.0.0
x86-64 clang 3.1
x86-64 clang 3.2
x86-64 clang 3.3
x86-64 clang 3.4.1
x86-64 clang 3.5
x86-64 clang 3.5.1
x86-64 clang 3.6
x86-64 clang 3.7
x86-64 clang 3.7.1
x86-64 clang 3.8
x86-64 clang 3.8.1
x86-64 clang 3.9.0
x86-64 clang 3.9.1
x86-64 clang 4.0.0
x86-64 clang 4.0.1
x86-64 clang 5.0.0
x86-64 clang 5.0.1
x86-64 clang 5.0.2
x86-64 clang 6.0.0
x86-64 clang 6.0.1
x86-64 clang 7.0.0
x86-64 clang 7.0.1
x86-64 clang 7.1.0
x86-64 clang 8.0.0
x86-64 clang 8.0.1
x86-64 clang 9.0.0
x86-64 clang 9.0.1
x86-64 gcc (static analysis)
x86-64 gcc (trunk)
x86-64 gcc 10.1
x86-64 gcc 10.2
x86-64 gcc 10.3
x86-64 gcc 4.1.2
x86-64 gcc 4.4.7
x86-64 gcc 4.5.3
x86-64 gcc 4.6.4
x86-64 gcc 4.7.1
x86-64 gcc 4.7.2
x86-64 gcc 4.7.3
x86-64 gcc 4.7.4
x86-64 gcc 4.8.1
x86-64 gcc 4.8.2
x86-64 gcc 4.8.3
x86-64 gcc 4.8.4
x86-64 gcc 4.8.5
x86-64 gcc 4.9.0
x86-64 gcc 4.9.1
x86-64 gcc 4.9.2
x86-64 gcc 4.9.3
x86-64 gcc 4.9.4
x86-64 gcc 5.1
x86-64 gcc 5.2
x86-64 gcc 5.3
x86-64 gcc 5.4
x86-64 gcc 6.1
x86-64 gcc 6.2
x86-64 gcc 6.3
x86-64 gcc 7.1
x86-64 gcc 7.2
x86-64 gcc 7.3
x86-64 gcc 8.1
x86-64 gcc 8.2
x86-64 gcc 8.3
x86-64 gcc 9.1
x86-64 gcc 9.2
x86-64 gcc 9.3
x86-64 icc 13.0.1
x86-64 icc 16.0.3
x86-64 icc 17.0.0
x86-64 icc 18.0.0
x86-64 icc 19.0.0
x86-64 icc 19.0.1
x86-64 icc 2021.1.2
x86-64 icx 2021.1.2
Options
Source code
#include <stdlib.h> // abort __attribute__((noinline)) __attribute__((warning("condition is not guaranteed"))) static void never_reach(void) { abort(); } // must define a side effect, to not be optimized away // EXPECT() : will trigger a warning if the condition is not guaranteed #define EXPECT(c) (void)((c) ? (void)0 : never_reach()) // assume() : tell the compiler that `cond` is true // note : only works for simple conditions, such as `i>=0`. // Avoid complex conditions invoking functions. #define assume(cond) do { if (!(cond)) __builtin_unreachable(); } while (0) // ********************************************************* // Function declaration // ********************************************************* int positive_plus1_body(int v); #define positive_plus1_preconditions(v) ((v)>=0) // Let's first define the preconditions. // Name is long, because conditions must be unique to the function // The inlined function express the contract, with both pre and post conditions. // `inline` is essential, so that actual input values get verified, // and result gets enriched with `assume` conditions. // Problem is, the error is now located INTO the inlined function, not at the place where it's called. // This makes it very hard to identify where the problem happens. static inline int positive_plus1(int v) // Ideally, this function should also have additional attribute to not trigger warnings when it's not invoked { int r; EXPECT(positive_plus1_preconditions(v)); // preconditions r = positive_plus1_body(v); assume(r > 0); // postconditions return r; } // Note : one consequence of this construction is that // there is no `positive_plus1()` function symbol in the library, // only positive_plus1_body(), which doesn't implement the contract. // Invoking positive_plus1() now requires the header file. // ********************************************************* // Usages // ********************************************************* int test11(void) { return positive_plus1(3); } // Fine : condition is respected int test12(int i) { if (i<0) return 0; return positive_plus1(i); } // after the `if`, i >= 0 necessarily, so `i` respects the condition => no warning int test13(int i) { if (i<2) return 0; i-=2; return positive_plus1(i); } // compiler can correctly track the range value of `i` after simple arithmetic # if 0 // Replace by 1 to trigger warnings due to incorrect invocations // The following usages will trigger warnings // Problem is, the error will be located _inside_ the inlined function, at EXPECT()'s position int test21(void) { return positive_plus1(-1); } // Condition not respected : triggers a warning int test22(int i) { return positive_plus1(i); } // No idea about value of `i` : it may not respect condition => correctly triggers a warning #endif // ********************************************************* // Function definition // ********************************************************* __attribute__((noinline)) int positive_plus1_body(int v) { assume(positive_plus1_preconditions(v)); // Re-use conditions defined in declaration, to keep synchronized return v+1; } int positive_plus2(int v) { assume(v>=0); v = positive_plus1(v); v = positive_plus1(v); // Without post-conditions, this second invocation would fail. // This can be tested by commenting out the postcondition line inside `positive_plus1()`. return v; }
Become a Patron
Sponsor on GitHub
Donate via PayPal
Source on GitHub
Mailing list
Installed libraries
Wiki
Report an issue
How it works
Contact the author
About the author
Changelog
Version tree