Skip to content

Commit 833ca9a

Browse files
committed
add clang's __builtin_assume
This adds a declaration for a clang builtin that tells the optimizer about a boolean invariant.
1 parent 62f1d5a commit 833ca9a

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/ansi-c/clang_builtin_headers.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -91,4 +91,6 @@ unsigned char __builtin_rotateright8(unsigned char, unsigned char);
9191
unsigned short __builtin_rotateright16(unsigned short, unsigned short);
9292
unsigned int __builtin_rotateright32(unsigned int, unsigned int);
9393
unsigned long long __builtin_rotateright64(unsigned long long, unsigned long long);
94+
95+
void __builtin_assume(__CPROVER_bool);
9496
// clang-format on

0 commit comments

Comments
 (0)