File tree Expand file tree Collapse file tree 3 files changed +57
-0
lines changed
regression/cbmc-library/__builtin_clz-02 Expand file tree Collapse file tree 3 files changed +57
-0
lines changed Original file line number Diff line number Diff line change
1
+ #ifdef _MSC_VER
2
+ # define __builtin_clz (x ) __lzcnt(x)
3
+ # define _Static_assert static_assert
4
+ #endif
5
+
6
+ int main ()
7
+ {
8
+ _Static_assert (
9
+ __builtin_clz (0xffU ) == 8 * sizeof (unsigned ) - 8 , "compile-time constant" );
10
+
11
+ return 0 ;
12
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ main.c
3
+
4
+ ^EXIT=0$
5
+ ^SIGNAL=0$
6
+ --
7
+ ^warning: ignoring
8
+ --
9
+ For this example, __builtin_clz is fully evaluated in the front-end. The
10
+ _Static_assert ensures this is the case, as type checking fails when
11
+ _Static_assert does not have a compile-time constant value.
Original file line number Diff line number Diff line change @@ -2591,6 +2591,40 @@ exprt c_typecheck_baset::do_special_functions(
2591
2591
2592
2592
return std::move (popcount_expr);
2593
2593
}
2594
+ else if (
2595
+ identifier == " __builtin_clz" || identifier == " __builtin_clzl" ||
2596
+ identifier == " __builtin_clzll" || identifier == " __lzcnt16" ||
2597
+ identifier == " __lzcnt" || identifier == " __lzcnt64" )
2598
+ {
2599
+ if (expr.arguments ().size () != 1 )
2600
+ {
2601
+ error ().source_location = f_op.source_location ();
2602
+ error () << identifier << " expects one operand" << eom;
2603
+ throw 0 ;
2604
+ }
2605
+
2606
+ side_effect_expr_function_callt try_constant{expr};
2607
+ typecheck_function_call_arguments (try_constant);
2608
+ exprt argument = try_constant.arguments ().front ();
2609
+ simplify (argument, *this );
2610
+ const auto int_constant = numeric_cast<mp_integer>(argument);
2611
+
2612
+ if (
2613
+ !int_constant.has_value () || *int_constant == 0 ||
2614
+ argument.type ().id () != ID_unsignedbv)
2615
+ {
2616
+ return nil_exprt{};
2617
+ }
2618
+
2619
+ const std::string binary_value = integer2binary (
2620
+ *int_constant, to_unsignedbv_type (argument.type ()).get_width ());
2621
+ std::size_t n_leading_zeros = binary_value.find (' 1' );
2622
+ CHECK_RETURN (n_leading_zeros != std::string::npos);
2623
+
2624
+ return from_integer (
2625
+ n_leading_zeros,
2626
+ to_code_type (try_constant.function ().type ()).return_type ());
2627
+ }
2594
2628
else if (identifier==CPROVER_PREFIX " equal" )
2595
2629
{
2596
2630
if (expr.arguments ().size ()!=2 )
You can’t perform that action at this time.
0 commit comments