Skip to content

Commit e4be101

Browse files
committed
Add support for __builtin_nondeterministic_value
Clang 17.0.1 introduced `__builtin_nondeterministic_value` to return a nondeterministic value of the same type as the provided argument.
1 parent 724f2f7 commit e4be101

File tree

2 files changed

+31
-0
lines changed

2 files changed

+31
-0
lines changed

regression/cbmc/gcc_vector3/main.c

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,14 @@ void test_shufflevector(void)
4242

4343
vector_u res;
4444

45+
# if defined(__clang__)
46+
// None of the indices refers to the second vector, so we can safely make it
47+
// non-deterministic.
48+
res.v = __builtin_shufflevector(
49+
a, __builtin_nondeterministic_value(a), 0, 1, -1, 3);
50+
# else
4551
res.v = __builtin_shufflevector(a, a, 0, 1, -1, 3);
52+
# endif
4653
assert(res.members[0] == 1);
4754
assert(res.members[1] == 2);
4855
// res.members[2] is "don't care"

src/ansi-c/c_typecheck_expr.cpp

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2185,6 +2185,30 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
21852185

21862186
return;
21872187
}
2188+
else if(
2189+
identifier == "__builtin_nondeterministic_value" &&
2190+
config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG)
2191+
{
2192+
// From Clang's documentation:
2193+
// Each call to __builtin_nondeterministic_value returns a valid value
2194+
// of the type given by the argument.
2195+
// Clang only supports integer types, floating-point types, vector
2196+
// types.
2197+
if(expr.arguments().size() != 1)
2198+
{
2199+
error().source_location = f_op.source_location();
2200+
error() << "__builtin_nondeterministic_value expects one operand"
2201+
<< eom;
2202+
throw 0;
2203+
}
2204+
typecheck_expr(expr.arguments().front());
2205+
2206+
side_effect_expr_nondett result{
2207+
expr.arguments().front().type(), f_op.source_location()};
2208+
expr.swap(result);
2209+
2210+
return;
2211+
}
21882212
else if(
21892213
identifier == "__builtin_shuffle" &&
21902214
config.ansi_c.mode == configt::ansi_ct::flavourt::GCC)

0 commit comments

Comments
 (0)