@@ -3396,21 +3396,6 @@ std::string expr2ct::convert_with_precedence(
3396
3396
else if (src.id ()==ID_unary_plus)
3397
3397
return convert_unary (to_unary_expr (src), " +" , precedence = 15 );
3398
3398
3399
- else if (src.id ()==ID_floatbv_plus)
3400
- return convert_function (src, " FLOAT+" );
3401
-
3402
- else if (src.id ()==ID_floatbv_minus)
3403
- return convert_function (src, " FLOAT-" );
3404
-
3405
- else if (src.id ()==ID_floatbv_mult)
3406
- return convert_function (src, " FLOAT*" );
3407
-
3408
- else if (src.id ()==ID_floatbv_div)
3409
- return convert_function (src, " FLOAT/" );
3410
-
3411
- else if (src.id ()==ID_floatbv_rem)
3412
- return convert_function (src, " FLOAT%" );
3413
-
3414
3399
else if (src.id ()==ID_floatbv_typecast)
3415
3400
{
3416
3401
const auto &floatbv_typecast = to_floatbv_typecast_expr (src);
@@ -3460,21 +3445,6 @@ std::string expr2ct::convert_with_precedence(
3460
3445
return convert_function (src, " __builtin_popcount" );
3461
3446
}
3462
3447
3463
- else if (src.id () == ID_r_ok)
3464
- return convert_function (src, " R_OK" );
3465
-
3466
- else if (src.id () == ID_w_ok)
3467
- return convert_function (src, " W_OK" );
3468
-
3469
- else if (src.id () == ID_is_invalid_pointer)
3470
- return convert_function (src, " IS_INVALID_POINTER" );
3471
-
3472
- else if (src.id ()==ID_good_pointer)
3473
- return convert_function (src, " GOOD_POINTER" );
3474
-
3475
- else if (src.id ()==ID_object_size)
3476
- return convert_function (src, " OBJECT_SIZE" );
3477
-
3478
3448
else if (src.id ()==" pointer_arithmetic" )
3479
3449
return convert_pointer_arithmetic (src, precedence=16 );
3480
3450
@@ -3492,85 +3462,18 @@ std::string expr2ct::convert_with_precedence(
3492
3462
return id2string (src.id ());
3493
3463
}
3494
3464
3495
- else if (src.id ()==ID_infinity)
3496
- return convert_function (src, " INFINITY" );
3497
-
3498
3465
else if (src.id ()==" builtin-function" )
3499
3466
return src.get_string (ID_identifier);
3500
3467
3501
- else if (src.id ()==ID_pointer_object)
3502
- return convert_function (src, " POINTER_OBJECT" );
3503
-
3504
- else if (src.id () == ID_get_must)
3505
- return convert_function (src, CPROVER_PREFIX " get_must" );
3506
-
3507
- else if (src.id () == ID_get_may)
3508
- return convert_function (src, CPROVER_PREFIX " get_may" );
3509
-
3510
- else if (src.id ()==" object_value" )
3511
- return convert_function (src, " OBJECT_VALUE" );
3512
-
3513
3468
else if (src.id ()==ID_array_of)
3514
3469
return convert_array_of (src, precedence=16 );
3515
3470
3516
- else if (src.id ()==ID_pointer_offset)
3517
- return convert_function (src, " POINTER_OFFSET" );
3518
-
3519
- else if (src.id ()==" pointer_base" )
3520
- return convert_function (src, " POINTER_BASE" );
3521
-
3522
- else if (src.id ()==" pointer_cons" )
3523
- return convert_function (src, " POINTER_CONS" );
3524
-
3525
- else if (src.id () == ID_is_invalid_pointer)
3526
- return convert_function (src, CPROVER_PREFIX " is_invalid_pointer" );
3527
-
3528
- else if (src.id () == ID_dynamic_object)
3529
- return convert_function (src, " DYNAMIC_OBJECT" );
3530
-
3531
- else if (src.id () == ID_is_dynamic_object)
3532
- return convert_function (src, " IS_DYNAMIC_OBJECT" );
3533
-
3534
- else if (src.id ()==" is_zero_string" )
3535
- return convert_function (src, " IS_ZERO_STRING" );
3536
-
3537
- else if (src.id ()==" zero_string" )
3538
- return convert_function (src, " ZERO_STRING" );
3539
-
3540
- else if (src.id ()==" zero_string_length" )
3541
- return convert_function (src, " ZERO_STRING_LENGTH" );
3542
-
3543
- else if (src.id ()==" buffer_size" )
3544
- return convert_function (src, " BUFFER_SIZE" );
3545
-
3546
- else if (src.id ()==ID_isnan)
3547
- return convert_function (src, " isnan" );
3548
-
3549
- else if (src.id ()==ID_isfinite)
3550
- return convert_function (src, " isfinite" );
3551
-
3552
- else if (src.id ()==ID_isinf)
3553
- return convert_function (src, " isinf" );
3554
-
3555
3471
else if (src.id ()==ID_bswap)
3556
3472
return convert_function (
3557
3473
src,
3558
3474
" __builtin_bswap" + integer2string (*pointer_offset_bits (
3559
3475
to_unary_expr (src).op ().type (), ns)));
3560
3476
3561
- else if (src.id ()==ID_isnormal)
3562
- return convert_function (src, " isnormal" );
3563
-
3564
- else if (src.id ()==ID_builtin_offsetof)
3565
- return convert_function (src, " builtin_offsetof" );
3566
-
3567
- else if (src.id ()==ID_gcc_builtin_va_arg)
3568
- return convert_function (src, " gcc_builtin_va_arg" );
3569
-
3570
- else if (src.id ()==ID_alignof)
3571
- // C uses "_Alignof", C++ uses "alignof"
3572
- return convert_function (src, " alignof" );
3573
-
3574
3477
else if (has_prefix (src.id_string (), " byte_extract" ))
3575
3478
return convert_byte_extract (to_byte_extract_expr (src), precedence = 16 );
3576
3479
@@ -3715,27 +3618,6 @@ std::string expr2ct::convert_with_precedence(
3715
3618
else if (src.id ()==ID_equal)
3716
3619
return convert_binary (to_equal_expr (src), " ==" , precedence = 9 , true );
3717
3620
3718
- else if (src.id ()==ID_ieee_float_equal)
3719
- return convert_function (src, " IEEE_FLOAT_EQUAL" );
3720
-
3721
- else if (src.id ()==ID_width)
3722
- return convert_function (src, " WIDTH" );
3723
-
3724
- else if (src.id ()==ID_concatenation)
3725
- return convert_function (src, " CONCATENATION" );
3726
-
3727
- else if (src.id ()==ID_ieee_float_notequal)
3728
- return convert_function (src, " IEEE_FLOAT_NOTEQUAL" );
3729
-
3730
- else if (src.id ()==ID_abs)
3731
- return convert_function (src, " abs" );
3732
-
3733
- else if (src.id ()==ID_complex_real)
3734
- return convert_function (src, " __real__" );
3735
-
3736
- else if (src.id ()==ID_complex_imag)
3737
- return convert_function (src, " __imag__" );
3738
-
3739
3621
else if (src.id ()==ID_complex)
3740
3622
return convert_complex (src, precedence=16 );
3741
3623
@@ -3896,8 +3778,58 @@ std::string expr2ct::convert_with_precedence(
3896
3778
else if (src.id ()==ID_type)
3897
3779
return convert (src.type ());
3898
3780
3899
- else if (src.id () == ID_count_leading_zeros)
3900
- return convert_function (src, " __builtin_clz" );
3781
+ return convert_function_or_norep (src, precedence);
3782
+ }
3783
+
3784
+ std::string
3785
+ expr2ct::convert_function_or_norep (const exprt &src, unsigned &precedence)
3786
+ {
3787
+ static const std::map<irep_idt, std::string> function_names = {
3788
+ {" buffer_size" , " BUFFER_SIZE" },
3789
+ {" is_zero_string" , " IS_ZERO_STRING" },
3790
+ {" object_value" , " OBJECT_VALUE" },
3791
+ {" pointer_base" , " POINTER_BASE" },
3792
+ {" pointer_cons" , " POINTER_CONS" },
3793
+ {" zero_string" , " ZERO_STRING" },
3794
+ {" zero_string_length" , " ZERO_STRING_LENGTH" },
3795
+ {ID_abs, " abs" },
3796
+ {ID_alignof, " alignof" }, // C uses "_Alignof", C++ uses "alignof"
3797
+ {ID_builtin_offsetof, " builtin_offsetof" },
3798
+ {ID_complex_imag, " __imag__" },
3799
+ {ID_complex_real, " __real__" },
3800
+ {ID_concatenation, " CONCATENATION" },
3801
+ {ID_count_leading_zeros, " __builtin_clz" },
3802
+ {ID_dynamic_object, " DYNAMIC_OBJECT" },
3803
+ {ID_floatbv_div, " FLOAT/" },
3804
+ {ID_floatbv_minus, " FLOAT-" },
3805
+ {ID_floatbv_mult, " FLOAT*" },
3806
+ {ID_floatbv_plus, " FLOAT+" },
3807
+ {ID_floatbv_rem, " FLOAT%" },
3808
+ {ID_gcc_builtin_va_arg, " gcc_builtin_va_arg" },
3809
+ {ID_get_may, CPROVER_PREFIX " get_may" },
3810
+ {ID_get_must, CPROVER_PREFIX " get_must" },
3811
+ {ID_good_pointer, " GOOD_POINTER" },
3812
+ {ID_ieee_float_equal, " IEEE_FLOAT_EQUAL" },
3813
+ {ID_ieee_float_notequal, " IEEE_FLOAT_NOTEQUAL" },
3814
+ {ID_infinity, " INFINITY" },
3815
+ {ID_is_dynamic_object, " IS_DYNAMIC_OBJECT" },
3816
+ {ID_is_invalid_pointer, " IS_INVALID_POINTER" },
3817
+ {ID_is_invalid_pointer, CPROVER_PREFIX " is_invalid_pointer" },
3818
+ {ID_isfinite, " isfinite" },
3819
+ {ID_isinf, " isinf" },
3820
+ {ID_isnan, " isnan" },
3821
+ {ID_isnormal, " isnormal" },
3822
+ {ID_object_size, " OBJECT_SIZE" },
3823
+ {ID_pointer_object, " POINTER_OBJECT" },
3824
+ {ID_pointer_offset, " POINTER_OFFSET" },
3825
+ {ID_r_ok, " R_OK" },
3826
+ {ID_w_ok, " W_OK" },
3827
+ {ID_width, " WIDTH" },
3828
+ };
3829
+
3830
+ const auto function_entry = function_names.find (src.id ());
3831
+ if (function_entry != function_names.end ())
3832
+ return convert_function (src, function_entry->second );
3901
3833
3902
3834
// no C language expression for internal representation
3903
3835
return convert_norep (src, precedence);
0 commit comments