CBMC: /home/runner/work/cbmc/cbmc/src/util/std

CBMC: /home/runner/work/cbmc/cbmc/src/util/std_expr.h Source File

10#ifndef CPROVER_UTIL_STD_EXPR_H

11#define CPROVER_UTIL_STD_EXPR_H

23{

24public:

31 const exprt &expr,

33 {

35 vm,

37 "nullary expression must not have operands");

38 }

41 const exprt &expr,

44 {

46 }

64};

68{

69public:

79 std::move(_type),

80 {std::move(_op0), std::move(_op1), std::move(_op2)})

81 {

82 }

93 const exprt &expr,

95 {

97 vm,

99 "ternary expression must have three operands");

100 }

101

103 const exprt &expr,

106 {

108 }

109};

110

122

129

132{

133public:

138

146

155

160

165

168 {

169 if(location.is_not_nil())

171 return *this;

172 }

173

176 {

177 if(location.is_not_nil())

179 return std::move(*this);

180 }

181

184 {

185 if(other.source_location().is_not_nil())

187 return *this;

188 }

189

192 {

193 if(other.source_location().is_not_nil())

195 return std::move(*this);

196 }

197};

198

199template <>

204

212{

215 return static_cast<const symbol_exprt &>(expr);

216}

217

225

226

227namespace std

228{

229template <>

230

238}

239

243{

244public:

251

256

261

266

271

276

281};

282

285{

286public:

294

307

312

317};

318

319template <>

324

329

342

350

351

354{

355public:

360

365

367 const exprt &expr,

369 {

371 vm,

373 "unary expression must have one operand");

374 }

375

377 const exprt &expr,

380 {

382 }

383

385 {

386 return op0();

387 }

388

390 {

391 return op0();

392 }

393

400};

401

402template <>

404{

405 return base.operands().size() == 1;

406}

407

415{

417 return static_cast<const unary_exprt &>(expr);

418}

419

426

427

436

437template <>

442

450{

453 return static_cast<const abs_exprt &>(expr);

454}

455

458{

461 return static_cast<abs_exprt &>(expr);

462}

463

464

467{

468public:

473

478};

479

480template <>

485

498

506

516

517template <>

522

535

543

547{

548public:

553

555 const exprt &expr,

557 {

558 }

559};

560

564{

565public:

570

572 const exprt &expr,

574 {

577 }

578};

579

591

598

609

610template <>

615

623{

626 return static_cast<const sign_exprt &>(expr);

627}

628

631{

634 return static_cast<sign_exprt &>(expr);

635}

636

639{

640public:

645

650

652 const exprt &expr,

654 {

656 vm,

658 "binary expression must have two operands");

659 }

660

662 const exprt &expr,

665 {

667 }

668

673

678

683

688

689

692

697};

698

699template <>

701{

702 return base.operands().size() == 2;

703}

704

712{

714 return static_cast<const binary_exprt &>(expr);

715}

716

723

727{

728public:

733

735 const exprt &expr,

737 {

740 }

741

743 const exprt &expr,

746 {

749 }

750};

751

763

770

774{

775public:

780

782 const exprt &expr,

784 {

786 }

787

789 const exprt &expr,

792 {

794

795

797

798

800 vm,

802 "lhs and rhs of binary relation expression should have same type");

803 }

804};

805

806template <>

811

823

830

840

841template <>

843{

844 return base.id() == ID_gt;

845}

846

856

857template <>

859{

860 return base.id() == ID_ge;

861}

862

872

873template <>

875{

876 return base.id() == ID_lt;

877}

878

888

889template <>

891{

892 return base.id() == ID_le;

893}

894

898{

899public:

905

913

918

923

924

925

931

937

943

949

955

961

967

973};

974

985

991

992

996{

997public:

1002

1008 std::move(_type))

1009 {

1010 }

1011

1016

1021};

1022

1023template <>

1028

1036{

1040 return ret;

1041}

1042

1045{

1049 return ret;

1050}

1051

1052

1062

1063template <>

1068

1076{

1079 return static_cast<const minus_exprt &>(expr);

1080}

1081

1084{

1087 return static_cast<minus_exprt &>(expr);

1088}

1089

1090

1094{

1095public:

1100

1105

1110};

1111

1112template <>

1117

1125{

1128 return static_cast<const mult_exprt &>(expr);

1129}

1130

1133{

1136 return static_cast<mult_exprt &>(expr);

1137}

1138

1139

1142{

1143public:

1148

1151 {

1152 return op0();

1153 }

1154

1157 {

1158 return op0();

1159 }

1160

1163 {

1164 return op1();

1165 }

1166

1169 {

1170 return op1();

1171 }

1172};

1173

1174template <>

1179

1187{

1190 return static_cast<const div_exprt &>(expr);

1191}

1192

1195{

1198 return static_cast<div_exprt &>(expr);

1199}

1200

1206{

1207public:

1212

1215 {

1216 return op0();

1217 }

1218

1221 {

1222 return op0();

1223 }

1224

1227 {

1228 return op1();

1229 }

1230

1233 {

1234 return op1();

1235 }

1236};

1237

1238template <>

1243

1251{

1254 return static_cast<const mod_exprt &>(expr);

1255}

1256

1259{

1262 return static_cast<mod_exprt &>(expr);

1263}

1264

1267{

1268public:

1273

1276 {

1277 return op0();

1278 }

1279

1282 {

1283 return op0();

1284 }

1285

1288 {

1289 return op1();

1290 }

1291

1294 {

1295 return op1();

1296 }

1297};

1298

1299template <>

1304

1317

1325

1326

1329{

1330public:

1336

1338 const exprt &expr,

1340 {

1342 }

1343

1345 const exprt &expr,

1348 {

1350 }

1351};

1352

1353template <>

1358

1366{

1369 return static_cast<const equal_exprt &>(expr);

1370}

1371

1374{

1377 return static_cast<equal_exprt &>(expr);

1378}

1379

1380

1390

1391template <>

1396

1409

1417

1418

1421{

1422public:

1423

1424

1425

1426

1438

1444 std::move(_type))

1445 {

1449 }

1450

1452 {

1453 return op0();

1454 }

1455

1457 {

1458 return op0();

1459 }

1460

1462 {

1463 return op1();

1464 }

1465

1467 {

1468 return op1();

1469 }

1470};

1471

1472template <>

1477

1485{

1488 return static_cast<const index_exprt &>(expr);

1489}

1490

1493{

1496 return static_cast<index_exprt &>(expr);

1497}

1498

1499

1502{

1503public:

1508

1513

1518

1520 {

1521 return op0();

1522 }

1523

1525 {

1526 return op0();

1527 }

1528};

1529

1530template <>

1535

1548

1556

1557

1560{

1561public:

1566

1571

1576

1578 {

1579 if(other.source_location().is_not_nil())

1581 return *this;

1582 }

1583

1585 {

1586 if(other.source_location().is_not_nil())

1588 return std::move(*this);

1589 }

1590};

1591

1592template <>

1597

1605{

1608 return static_cast<const array_exprt &>(expr);

1609}

1610

1613{

1616 return static_cast<array_exprt &>(expr);

1617}

1618

1622{

1623public:

1628

1633

1638

1644

1646 const exprt &expr,

1648 {

1650 vm, expr.operands().size() % 2 == 0, "number of operands must be even");

1651 }

1652};

1653

1654template <>

1659

1666

1673

1683

1684template <>

1689

1697{

1700 return static_cast<const vector_exprt &>(expr);

1701}

1702

1710

1711

1714{

1715public:

1721

1726

1731

1736

1741};

1742

1743template <>

1748

1756{

1759 return static_cast<const union_exprt &>(expr);

1760}

1761

1764{

1767 return static_cast<union_exprt &>(expr);

1768}

1769

1780

1781template <>

1786

1799

1807

1810{

1811public:

1816

1819};

1820

1821template <>

1826

1834{

1836 return static_cast<const struct_exprt &>(expr);

1837}

1838

1845

1846

1849{

1850public:

1856 std::move(_type))

1857 {

1858 }

1859

1861 {

1862 return op0();

1863 }

1864

1866 {

1867 return op0();

1868 }

1869

1871 {

1872 return op1();

1873 }

1874

1876 {

1877 return op1();

1878 }

1879};

1880

1881template <>

1886

1894{

1897 return static_cast<const complex_exprt &>(expr);

1898}

1899

1907

1917

1918template <>

1923

1936

1944

1954

1955template <>

1960

1973

1981

1982

1985{

1986public:

1991

1992

1994 {

1996 return expr;

1997 else

1999 }

2000};

2001

2002template <>

2007

2020

2028

2033{

2034public:

2039

2043 {std::move(op0), std::move(op1), std::move(op2)},

2045 {

2046 }

2047

2051 {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},

2053 {

2054 }

2055

2060};

2061

2065

2067

2072

2073template <>

2078

2086{

2089 return static_cast<const and_exprt &>(expr);

2090}

2091

2094{

2097 return static_cast<and_exprt &>(expr);

2098}

2099

2108{

2109public:

2114

2119};

2120

2128{

2131 return static_cast<const nand_exprt &>(expr);

2132}

2133

2136{

2139 return static_cast<nand_exprt &>(expr);

2140}

2141

2151

2152template <>

2157

2165{

2168 return static_cast<const implies_exprt &>(expr);

2169}

2170

2178

2183{

2184public:

2189

2193 {std::move(op0), std::move(op1), std::move(op2)},

2195 {

2196 }

2197

2201 {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},

2203 {

2204 }

2205

2210};

2211

2215

2217

2218template <>

2220{

2221 return base.id() == ID_or;

2222}

2223

2231{

2234 return static_cast<const or_exprt &>(expr);

2235}

2236

2239{

2242 return static_cast<or_exprt &>(expr);

2243}

2244

2253{

2254public:

2259

2264};

2265

2273{

2276 return static_cast<const nor_exprt &>(expr);

2277}

2278

2281{

2283 return static_cast<nor_exprt &>(expr);

2284}

2285

2290{

2291public:

2296

2301};

2302

2303template <>

2308

2316{

2319 return static_cast<const xor_exprt &>(expr);

2320}

2321

2324{

2327 return static_cast<xor_exprt &>(expr);

2328}

2329

2336{

2337public:

2342

2347};

2348

2349template <>

2354

2362{

2365 return static_cast<const xnor_exprt &>(expr);

2366}

2367

2370{

2373 return static_cast<xnor_exprt &>(expr);

2374}

2375

2385

2386template <>

2391

2399{

2402 return static_cast<const not_exprt &>(expr);

2403}

2404

2407{

2410 return static_cast<not_exprt &>(expr);

2411}

2412

2413

2416{

2417public:

2422

2427 std::move(t),

2428 std::move(f),

2430 {

2431 }

2432

2434 {

2435 return op0();

2436 }

2437

2439 {

2440 return op0();

2441 }

2442

2444 {

2445 return op1();

2446 }

2447

2449 {

2450 return op1();

2451 }

2452

2454 {

2455 return op2();

2456 }

2457

2459 {

2460 return op2();

2461 }

2462

2464 const exprt &expr,

2466 {

2468 }

2469

2471 const exprt &expr,

2474 {

2476 }

2477};

2478

2479template <>

2481{

2482 return base.id() == ID_if;

2483}

2484

2492{

2495 return static_cast<const if_exprt &>(expr);

2496}

2497

2500{

2503 return static_cast<if_exprt &>(expr);

2504}

2505

2510{

2511public:

2519

2521 {

2522 return op0();

2523 }

2524

2526 {

2527 return op0();

2528 }

2529

2531 {

2532 return op1();

2533 }

2534

2536 {

2537 return op1();

2538 }

2539

2541 {

2542 return op2();

2543 }

2544

2546 {

2547 return op2();

2548 }

2549};

2550

2551template <>

2556

2564{

2567 return static_cast<const with_exprt &>(expr);

2568}

2569

2572{

2575 return static_cast<with_exprt &>(expr);

2576}

2577

2579{

2580public:

2585

2587 {

2588 return op0();

2589 }

2590

2592 {

2593 return op0();

2594 }

2595};

2596

2597template <>

2602

2615

2623

2625{

2626public:

2632

2637};

2638

2639template <>

2644

2657

2665

2666

2669{

2670public:

2680

2682 {

2683 return op0();

2684 }

2685

2687 {

2688 return op0();

2689 }

2690

2691

2692

2693

2694

2699

2704

2706 {

2707 return op2();

2708 }

2709

2711 {

2712 return op2();

2713 }

2714

2717

2719 const exprt &expr,

2721 {

2723 }

2724

2726 const exprt &expr,

2729 {

2731 }

2732};

2733

2734template <>

2739

2741{

2743 value, 3, "Array/structure update must have three operands");

2744}

2745

2753{

2756 return static_cast<const update_exprt &>(expr);

2757}

2758

2766

2767

2768#if 0

2771{

2772public:

2778 {

2780 }

2781

2783 {

2784 operands().resize(3);

2785 }

2786

2788 {

2789 return op0();

2790 }

2791

2792 const exprt &array() const

2793 {

2794 return op0();

2795 }

2796

2798 {

2799 return op1();

2800 }

2801

2802 const exprt &index() const

2803 {

2804 return op1();

2805 }

2806

2807 exprt &new_value()

2808 {

2809 return op2();

2810 }

2811

2812 const exprt &new_value() const

2813 {

2814 return op2();

2815 }

2816};

2817

2819{

2821}

2822

2824{

2825 validate_operands(value, 3, "Array update must have three operands");

2826}

2827

2835{

2839 return ret;

2840}

2841

2844{

2848 return ret;

2849}

2850

2851#endif

2852

2853

2856{

2857public:

2867

2877

2882

2887

2892

2893

2895 {

2896 return op0();

2897 }

2898

2899

2901 {

2902 return op0();

2903 }

2904

2906 {

2907 return op0();

2908 }

2909

2911 {

2912 return op0();

2913 }

2914

2916 const exprt &expr,

2918 {

2920 vm,

2921 expr.operands().size() == 1,

2922 "member expression must have one operand");

2923 }

2924

2926 const exprt &expr,

2929};

2930

2931template <>

2936

2944{

2947 return static_cast<const member_exprt &>(expr);

2948}

2949

2957

2958

2967

2968template <>

2973

2981{

2984 return static_cast<const type_exprt &>(expr);

2985}

2986

2989{

2992 return static_cast<type_exprt &>(expr);

2993}

2994

2997{

2998public:

3004

3009

3014

3019

3020 using irept::operator==;

3021 using irept::operator!=;

3031 bool operator==(std::nullptr_t) const;

3033 bool operator!=(std::nullptr_t) const;

3034

3035 static void check(

3036 const exprt &expr,

3038

3040 const exprt &expr,

3043 {

3044 check(expr, vm);

3045 }

3046

3047protected:

3049};

3050

3051template <>

3056

3061

3074

3082

3086

3090

3103

3106

3110

3113

3122

3131

3141

3142template <>

3147

3157

3160{

3161public:

3163

3177 std::move(_type))

3178 {

3179 }

3180

3185

3190

3192 {

3193 return op1();

3194 }

3195

3197 {

3198 return op1();

3199 }

3200

3204

3208};

3209

3210template <>

3216

3224{

3229 return static_cast<const binding_exprt &>(expr);

3230}

3231

3246

3249{

3250public:

3267

3276

3281

3286

3294

3302

3305 {

3308 return values.front();

3309 }

3310

3313 {

3316 return values.front();

3317 }

3318

3323

3328

3334

3340

3346

3352

3354};

3355

3356template <>

3361

3366

3374{

3377 return static_cast<const let_exprt &>(expr);

3378}

3379

3382{

3385 return static_cast<let_exprt &>(expr);

3386}

3387

3388

3393{

3394public:

3399

3404 {

3407 operands().push_back(condition);

3408 operands().push_back(value);

3409 }

3410

3411

3413};

3414

3415template <>

3420

3422{

3424 value.operands().size() % 2 == 0, "cond must have even number of operands");

3425}

3426

3434{

3437 return static_cast<const cond_exprt &>(expr);

3438}

3439

3442{

3445 return static_cast<cond_exprt &>(expr);

3446}

3447

3453

3456{

3457public:

3462

3468

3475

3482

3488 {

3490 operands().push_back(case_value);

3491 operands().push_back(result_value);

3492 }

3493

3496 {

3498 return (operands().size() - 1) / 2;

3499 }

3500

3503 {

3505 return operands()[1 + 2 * i];

3506 }

3507

3510 {

3512 return operands()[1 + 2 * i];

3513 }

3514

3517 {

3519 return operands()[1 + 2 * i + 1];

3520 }

3521

3524 {

3526 return operands()[1 + 2 * i + 1];

3527 }

3528

3530 {

3532 expr.operands().size() >= 1,

3533 "case expression must have at least one operand");

3535 expr.operands().size() % 2 == 1,

3536 "case expression must have odd number of operands");

3537 }

3538};

3539

3540template <>

3545

3553{

3556 return static_cast<const case_exprt &>(expr);

3557}

3558

3561{

3564 return static_cast<case_exprt &>(expr);

3565}

3566

3576{

3577public:

3584 {std::move(arg)},

3585 std::move(body),

3586 std::move(_type))

3587 {

3588 }

3589

3594

3599

3606

3613

3618

3623};

3624

3625template <>

3630

3644

3652

3654

3657{

3658public:

3687

3698

3706

3713

3721};

3722

3724{

3725 validate_operands(value, 0, "class method descriptor must not have operands");

3728 "class method descriptor must have a mangled method name.");

3730 !value.class_id().empty(), "class method descriptor must have a class id.");

3733 "class method descriptor must have a base method name.");

3737 "class method descriptor must have an identifier in the expected format.");

3738}

3739

3753

3754template <>

3759

3766{

3767public:

3772 value,

3774 {

3776 }

3777

3782

3787

3789 {

3790 return op1();

3791 }

3792

3794 {

3795 return op1();

3796 }

3797};

3798

3799template <>

3804

3817

3825

3826#endif

const T & as_const(T &value)

Return a reference to the same object but ensures the type is const.

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Boolean AND All operands must be boolean, and the result is always boolean.

and_exprt(exprt op0, exprt op1, exprt op2)

and_exprt(exprt op0, exprt op1)

and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)

and_exprt(exprt::operandst _operands)

Expression to define a mapping from an argument (index) to elements.

const array_typet & type() const

const symbol_exprt & arg() const

const exprt & body() const

array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)

Array constructor from list of elements.

array_exprt && with_source_location(const exprt &other) &&

const array_typet & type() const

array_exprt & with_source_location(const exprt &other) &

array_exprt(operandst _operands, array_typet _type)

Array constructor from a list of index-element pairs Operands are index/value pairs,...

static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

void add(exprt index, exprt value)

add an index/value pair

const array_typet & type() const

array_list_exprt(operandst _operands, array_typet _type)

Array constructor from single element.

array_of_exprt(exprt _what, array_typet _type)

const exprt & what() const

const array_typet & type() const

A base class for binary expressions.

binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)

static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)

const exprt & op2() const =delete

static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

const exprt & lhs() const

binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)

const exprt & rhs() const

const exprt & op3() const =delete

A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...

static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)

static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)

A base class for relations, i.e., binary predicates whose two operands have the same type.

binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)

static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)

A base class for variable bindings (quantifiers, let, lambda)

const variablest & variables() const

const exprt & where() const

binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)

construct the binding expression

exprt instantiate(const exprt::operandst &) const

substitute free occurrences of the variables in where() by the given values

std::vector< symbol_exprt > variablest

Case expression: evaluates to the value corresponding to the first matching case.

exprt & result_value(std::size_t i)

Get the result value for the i-th case.

void add_case(const exprt &case_value, const exprt &result_value)

Add a case: value to compare and corresponding result.

const exprt & case_value(std::size_t i) const

Get the case value for the i-th case.

case_exprt(operandst _operands, typet _type)

exprt & select_value()

Get the value that is being compared against.

const exprt & result_value(std::size_t i) const

Get the result value for the i-th case.

std::size_t number_of_cases() const

Get the number of cases (excluding the select value)

case_exprt(exprt _select_value, typet _type)

Constructor with select value.

static void check(const exprt &expr)

exprt & case_value(std::size_t i)

Get the case value for the i-th case.

const exprt & select_value() const

Get the value that is being compared against.

An expression describing a method on a class.

const irep_idt & base_method_name() const

The name of the method to which this expression is applied as would be seen in the source code.

const irep_idt & mangled_method_name() const

The method name after mangling it by combining it with the descriptor.

const irep_idt & get_identifier() const

A unique identifier of the combination of class and method overload to which this expression refers.

class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)

const irep_idt & class_id() const

Unique identifier in the symbol table, of the compile time type of the class which this expression is...

Complex constructor from a pair of numbers.

complex_exprt(exprt _real, exprt _imag, complex_typet _type)

const exprt & real() const

const exprt & imag() const

Imaginary part of the expression describing a complex number.

complex_imag_exprt(const exprt &op)

Real part of the expression describing a complex number.

complex_real_exprt(const exprt &op)

Complex numbers made of pair of given subtype.

this is a parametric version of an if-expression: it returns the value of the first case (using the o...

void add_case(const exprt &condition, const exprt &value)

adds a case to a cond expression

cond_exprt(operandst _operands, typet _type)

A constant literal expression.

static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)

const irep_idt & get_value() const

bool operator!=(bool rhs) const

Return whether the expression lhs is not a constant of Boolean type or is not representing the Boolea...

bool value_is_zero_string() const

bool operator==(bool rhs) const

Return whether the expression lhs is a constant of Boolean type that is representing the Boolean valu...

constant_exprt(const irep_idt &_value, typet _type)

void set_value(const irep_idt &value)

bool is_null_pointer() const

Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...

static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...

void clear_thread_local()

decorated_symbol_exprt(const irep_idt &identifier, typet type)

void set_static_lifetime()

bool is_static_lifetime() const

bool is_thread_local() const

void clear_static_lifetime()

div_exprt(exprt _lhs, exprt _rhs)

exprt & dividend()

The dividend of a division is the number that is being divided.

const exprt & dividend() const

The dividend of a division is the number that is being divided.

const exprt & divisor() const

The divisor of a division is the number the dividend is being divided by.

exprt & divisor()

The divisor of a division is the number the dividend is being divided by.

dstringt has one field, an unsigned integer no which is an index into a static table of strings.

Union constructor to support unions without any member (a GCC/Clang feature).

empty_union_exprt(typet _type)

static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

equal_exprt(exprt _lhs, exprt _rhs)

static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)

Boute's Euclidean definition of Modulo – to match SMT-LIB2.

exprt & divisor()

The divisor of a division is the number the dividend is being divided by.

euclidean_mod_exprt(exprt _lhs, exprt _rhs)

const exprt & divisor() const

The divisor of a division is the number the dividend is being divided by.

exprt & dividend()

The dividend of a division is the number that is being divided.

const exprt & dividend() const

The dividend of a division is the number that is being divided.

Base class for all expressions.

std::vector< exprt > operandst

static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)

Check that the expression is well-formed, assuming that its subexpressions and type have all ready be...

bool is_boolean() const

Return whether the expression represents a Boolean.

bool is_constant() const

Return whether the expression is a constant.

typet & type()

Return the type of the expression.

static void check(const exprt &, const validation_modet=validation_modet::INVARIANT)

Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are ...

source_locationt & add_source_location()

void add_to_operands(const exprt &expr)

Add the given argument to the end of exprt's operands.

The Boolean constant false.

Binary greater than operator expression.

greater_than_exprt(exprt _lhs, exprt _rhs)

Binary greater than or equal operator expression.

greater_than_or_equal_exprt(exprt _lhs, exprt _rhs)

The trinary if-then-else operator.

const exprt & false_case() const

const exprt & cond() const

if_exprt(exprt cond, const exprt &t, exprt f)

const exprt & true_case() const

if_exprt(exprt cond, exprt t, exprt f, typet type)

static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)

implies_exprt(exprt op0, exprt op1)

const exprt & index() const

index_designatort(exprt _index)

index_exprt(exprt _array, exprt _index, typet _type)

index_exprt(const exprt &_array, exprt _index)

const exprt & index() const

const exprt & array() const

An expression denoting infinity.

infinity_exprt(typet _type)

bool get_bool(const irep_idt &name) const

std::size_t get_size_t(const irep_idt &name) const

const irep_idt & get(const irep_idt &name) const

void remove(const irep_idt &name)

void set(const irep_idt &name, const irep_idt &value)

void set_size_t(const irep_idt &name, const std::size_t value)

const irep_idt & id() const

Binary less than operator expression.

less_than_exprt(exprt _lhs, exprt _rhs)

Binary less than or equal operator expression.

less_than_or_equal_exprt(exprt _lhs, exprt _rhs)

binding_exprt::variablest & variables()

convenience accessor for binding().variables()

const binding_exprt & binding() const

const binding_exprt::variablest & variables() const

convenience accessor for binding().variables()

let_exprt(symbol_exprt symbol, exprt value, const exprt &where)

convenience constructor for the case of a single binding

const exprt & where() const

convenience accessor for binding().where()

static void validate(const exprt &, validation_modet)

const symbol_exprt & symbol() const

convenience accessor for the symbol of a single binding

let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)

exprt & value()

convenience accessor for the value of a single binding

exprt & where()

convenience accessor for binding().where()

binding_exprt & binding()

const operandst & values() const

const exprt & value() const

convenience accessor for the value of a single binding

symbol_exprt & symbol()

convenience accessor for the symbol of a single binding

irep_idt get_component_name() const

member_designatort(const irep_idt &_component_name)

Extract member of struct or union.

const exprt & compound() const

const exprt & struct_op() const

irep_idt get_component_name() const

void set_component_name(const irep_idt &component_name)

static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)

Check that the member expression has the right number of operands, refers to a component that exists ...

static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

member_exprt(exprt op, const irep_idt &component_name, typet _type)

std::size_t get_component_number() const

member_exprt(exprt op, const struct_typet::componentt &c)

minus_exprt(exprt _lhs, exprt _rhs)

Modulo defined as lhs-(rhs * truncate(lhs/rhs)).

exprt & dividend()

The dividend of a division is the number that is being divided.

const exprt & dividend() const

The dividend of a division is the number that is being divided.

exprt & divisor()

The divisor of a division is the number the dividend is being divided by.

const exprt & divisor() const

The divisor of a division is the number the dividend is being divided by.

mod_exprt(exprt _lhs, exprt _rhs)

Binary multiplication Associativity is not specified.

mult_exprt(exprt::operandst factors, typet type)

mult_exprt(exprt _lhs, exprt _rhs)

mult_exprt(exprt::operandst factors)

A base class for multi-ary expressions Associativity is not specified.

const exprt & op0() const

multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)

const exprt & op2() const

const exprt & op3() const

multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)

multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)

const exprt & op1() const

multi_ary_exprt(const irep_idt &_id, operandst _operands)

Expression that introduces a new symbol that is equal to the operand.

named_term_exprt(symbol_exprt symbol, exprt value)

const exprt & value() const

const symbol_exprt & symbol() const

A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...

nand_exprt(exprt op0, exprt op1)

nand_exprt(exprt::operandst _operands)

Expression to hold a nondeterministic choice.

void set_identifier(const irep_idt &identifier)

nondet_symbol_exprt(const irep_idt &identifier, typet type)

const irep_idt & get_identifier() const

nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)

nor_exprt(exprt op0, exprt op1)

nor_exprt(exprt::operandst _operands)

notequal_exprt(exprt _lhs, exprt _rhs)

An expression without operands.

static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)

const exprt & op1() const =delete

nullary_exprt(const irep_idt &_id, typet _type)

const exprt & op0() const =delete

void copy_to_operands(const exprt &, const exprt &, const exprt &)=delete

void copy_to_operands(const exprt &expr)=delete

operandst & operands()=delete

remove all operand methods

void copy_to_operands(const exprt &, const exprt &)=delete

const operandst & operands() const =delete

const exprt & op3() const =delete

const exprt & op2() const =delete

Boolean OR All operands must be boolean, and the result is always boolean.

or_exprt(exprt op0, exprt op1, exprt op2)

or_exprt(exprt::operandst _operands)

or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)

or_exprt(exprt op0, exprt op1)

The plus expression Associativity is not specified.

plus_exprt(exprt _lhs, exprt _rhs, typet _type)

plus_exprt(exprt _lhs, exprt _rhs)

plus_exprt(operandst _operands, typet _type)

plus_exprt(operandst _operands)

A base class for expressions that are predicates, i.e., Boolean-typed.

predicate_exprt(const irep_idt &_id)

static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

Sign of an expression Predicate is true if _op is negative, false otherwise.

Struct constructor from list of elements.

exprt & component(const irep_idt &name, const namespacet &ns)

struct_exprt(operandst _operands, typet _type)

Expression to hold a symbol (variable)

void set_identifier(const irep_idt &identifier)

static symbol_exprt typeless(const irep_idt &id)

Generate a symbol_exprt without a proper type.

symbol_exprt & with_source_location(const exprt &other) &

Add the source location from other, if it has any.

symbol_exprt & with_source_location(source_locationt location) &

Add the source location from location, if it is non-nil.

symbol_exprt && with_source_location(source_locationt location) &&

Add the source location from location, if it is non-nil.

symbol_exprt && with_source_location(const exprt &other) &&

Add the source location from other, if it has any.

symbol_exprt(const irep_idt &identifier, typet type)

const irep_idt & get_identifier() const

An expression with three operands.

static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)

ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)

const exprt & op3() const =delete

static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

The Boolean constant true.

An expression denoting a type.

Semantic type conversion.

static exprt conditional_cast(const exprt &expr, const typet &type)

typecast_exprt(exprt op, typet _type)

The type of an expression, extends irept.

Generic base class for unary expressions.

unary_exprt(const irep_idt &_id, const exprt &_op)

const exprt & op3() const =delete

static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

const exprt & op1() const =delete

unary_exprt(const irep_idt &_id, exprt _op, typet _type)

const exprt & op2() const =delete

static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)

The unary minus expression.

unary_minus_exprt(exprt _op)

unary_minus_exprt(exprt _op, typet _type)

The unary plus expression.

unary_plus_exprt(exprt op)

A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...

static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

unary_predicate_exprt(const irep_idt &_id, exprt _op)

Union constructor from single element.

std::size_t get_component_number() const

void set_component_number(std::size_t component_number)

void set_component_name(const irep_idt &component_name)

irep_idt get_component_name() const

union_exprt(const irep_idt &_component_name, exprt _value, typet _type)

Operator to update elements in structs and arrays.

with_exprt make_with_expr() const

converts an update expr into a (possibly nested) with expression

exprt::operandst & designator()

static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)

const exprt & new_value() const

update_exprt(const exprt &_old, exprt _designator, exprt _new_value)

static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)

const exprt & old() const

const exprt::operandst & designator() const

Vector constructor from list of elements.

vector_exprt(operandst _operands, vector_typet _type)

Operator to update elements in structs and arrays.

const exprt & old() const

const exprt & where() const

with_exprt(const exprt &_old, exprt _where, exprt _new_value)

const exprt & new_value() const

xnor_exprt(exprt::operandst _operands)

xnor_exprt(exprt _op0, exprt _op1)

Boolean XOR All operands must be boolean, and the result is always boolean.

xor_exprt(exprt _op0, exprt _op1)

xor_exprt(exprt::operandst _operands)

#define SINCE(year, month, day, msg)

Templated functions to cast to specific exprt-derived classes.

void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)

const irept & get_nil_irep()

dstring_hash irep_id_hash

const std::string & id2string(const irep_idt &d)

#define DATA_INVARIANT(CONDITION, REASON)

This condition should be used to document that assumptions that are made on goto_functions,...

#define PRECONDITION(CONDITION)

bool can_cast_expr< equal_exprt >(const exprt &base)

bool can_cast_expr< notequal_exprt >(const exprt &base)

bool can_cast_expr< complex_exprt >(const exprt &base)

bool can_cast_expr< not_exprt >(const exprt &base)

const struct_exprt & to_struct_expr(const exprt &expr)

Cast an exprt to a struct_exprt.

const array_list_exprt & to_array_list_expr(const exprt &expr)

bool can_cast_expr< typecast_exprt >(const exprt &base)

bool operator==(const exprt &lhs, bool rhs)

Return whether the expression lhs is a constant of Boolean type that is representing the Boolean valu...

const type_exprt & to_type_expr(const exprt &expr)

Cast an exprt to an type_exprt.

const array_of_exprt & to_array_of_expr(const exprt &expr)

Cast an exprt to an array_of_exprt.

bool can_cast_expr< struct_exprt >(const exprt &base)

const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)

Cast an exprt to a binary_relation_exprt.

const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)

Cast an exprt to a unary_plus_exprt.

bool can_cast_expr< xor_exprt >(const exprt &base)

const index_exprt & to_index_expr(const exprt &expr)

Cast an exprt to an index_exprt.

bool can_cast_expr< mult_exprt >(const exprt &base)

bool can_cast_expr< if_exprt >(const exprt &base)

const binary_predicate_exprt & to_binary_predicate_expr(const exprt &expr)

Cast an exprt to a binary_predicate_exprt.

const class_method_descriptor_exprt & to_class_method_descriptor_expr(const exprt &expr)

Cast an exprt to a class_method_descriptor_exprt.

bool can_cast_expr< named_term_exprt >(const exprt &base)

bool can_cast_expr< binding_exprt >(const exprt &base)

const mod_exprt & to_mod_expr(const exprt &expr)

Cast an exprt to a mod_exprt.

const mult_exprt & to_mult_expr(const exprt &expr)

Cast an exprt to a mult_exprt.

const and_exprt & to_and_expr(const exprt &expr)

Cast an exprt to a and_exprt.

bool can_cast_expr< member_designatort >(const exprt &base)

const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)

Cast an exprt to a array_comprehension_exprt.

const ternary_exprt & to_ternary_expr(const exprt &expr)

Cast an exprt to a ternary_exprt.

const named_term_exprt & to_named_term_expr(const exprt &expr)

Cast an exprt to a named_term_exprt.

const xnor_exprt & to_xnor_expr(const exprt &expr)

Cast an exprt to a xnor_exprt.

bool can_cast_expr< xnor_exprt >(const exprt &base)

bool can_cast_expr< array_comprehension_exprt >(const exprt &base)

const xor_exprt & to_xor_expr(const exprt &expr)

Cast an exprt to a xor_exprt.

const or_exprt & to_or_expr(const exprt &expr)

Cast an exprt to a or_exprt.

const array_exprt & to_array_expr(const exprt &expr)

Cast an exprt to an array_exprt.

bool can_cast_expr< complex_imag_exprt >(const exprt &base)

bool can_cast_expr< abs_exprt >(const exprt &base)

bool can_cast_expr< sign_exprt >(const exprt &base)

const unary_predicate_exprt & to_unary_predicate_expr(const exprt &expr)

Cast an exprt to a unary_predicate_exprt.

const cond_exprt & to_cond_expr(const exprt &expr)

Cast an exprt to a cond_exprt.

bool can_cast_expr< type_exprt >(const exprt &base)

exprt disjunction(const exprt::operandst &)

1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...

bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)

const typecast_exprt & to_typecast_expr(const exprt &expr)

Cast an exprt to a typecast_exprt.

const div_exprt & to_div_expr(const exprt &expr)

Cast an exprt to a div_exprt.

bool can_cast_expr< unary_minus_exprt >(const exprt &base)

bool can_cast_expr< less_than_exprt >(const exprt &base)

bool can_cast_expr< with_exprt >(const exprt &base)

const vector_exprt & to_vector_expr(const exprt &expr)

Cast an exprt to an vector_exprt.

exprt conjunction(const exprt::operandst &)

1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...

bool can_cast_expr< minus_exprt >(const exprt &base)

bool can_cast_expr< let_exprt >(const exprt &base)

const binary_exprt & to_binary_expr(const exprt &expr)

Cast an exprt to a binary_exprt.

const plus_exprt & to_plus_expr(const exprt &expr)

Cast an exprt to a plus_exprt.

const notequal_exprt & to_notequal_expr(const exprt &expr)

Cast an exprt to an notequal_exprt.

bool can_cast_expr< plus_exprt >(const exprt &base)

const nand_exprt & to_nand_expr(const exprt &expr)

Cast an exprt to a nand_exprt.

const unary_exprt & to_unary_expr(const exprt &expr)

Cast an exprt to a unary_exprt.

const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)

Cast an exprt to a multi_ary_exprt.

bool can_cast_expr< array_of_exprt >(const exprt &base)

const let_exprt & to_let_expr(const exprt &expr)

Cast an exprt to a let_exprt.

const abs_exprt & to_abs_expr(const exprt &expr)

Cast an exprt to a abs_exprt.

bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)

bool can_cast_expr< case_exprt >(const exprt &base)

bool can_cast_expr< constant_exprt >(const exprt &base)

const if_exprt & to_if_expr(const exprt &expr)

Cast an exprt to an if_exprt.

const member_exprt & to_member_expr(const exprt &expr)

Cast an exprt to a member_exprt.

void validate_expr(const nondet_symbol_exprt &value)

bool can_cast_expr< index_exprt >(const exprt &base)

bool can_cast_expr< symbol_exprt >(const exprt &base)

const empty_union_exprt & to_empty_union_expr(const exprt &expr)

Cast an exprt to an empty_union_exprt.

const minus_exprt & to_minus_expr(const exprt &expr)

Cast an exprt to a minus_exprt.

bool can_cast_expr< member_exprt >(const exprt &base)

bool can_cast_expr< empty_union_exprt >(const exprt &base)

const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)

Cast an exprt to a complex_imag_exprt.

const binding_exprt & to_binding_expr(const exprt &expr)

Cast an exprt to a binding_exprt.

bool can_cast_expr< or_exprt >(const exprt &base)

bool can_cast_expr< mod_exprt >(const exprt &base)

const index_designatort & to_index_designator(const exprt &expr)

Cast an exprt to an index_designatort.

const union_exprt & to_union_expr(const exprt &expr)

Cast an exprt to a union_exprt.

bool can_cast_expr< cond_exprt >(const exprt &base)

const complex_real_exprt & to_complex_real_expr(const exprt &expr)

Cast an exprt to a complex_real_exprt.

bool can_cast_expr< update_exprt >(const exprt &base)

bool can_cast_expr< binary_relation_exprt >(const exprt &base)

bool can_cast_expr< euclidean_mod_exprt >(const exprt &base)

bool can_cast_expr< vector_exprt >(const exprt &base)

const case_exprt & to_case_expr(const exprt &expr)

Cast an exprt to a case_exprt.

const constant_exprt & to_constant_expr(const exprt &expr)

Cast an exprt to a constant_exprt.

bool can_cast_expr< array_list_exprt >(const exprt &base)

bool can_cast_expr< index_designatort >(const exprt &base)

const not_exprt & to_not_expr(const exprt &expr)

Cast an exprt to an not_exprt.

const symbol_exprt & to_symbol_expr(const exprt &expr)

Cast an exprt to a symbol_exprt.

const with_exprt & to_with_expr(const exprt &expr)

Cast an exprt to a with_exprt.

const complex_exprt & to_complex_expr(const exprt &expr)

Cast an exprt to a complex_exprt.

bool can_cast_expr< unary_plus_exprt >(const exprt &base)

bool can_cast_expr< and_exprt >(const exprt &base)

bool can_cast_expr< greater_than_exprt >(const exprt &base)

const implies_exprt & to_implies_expr(const exprt &expr)

Cast an exprt to a implies_exprt.

bool can_cast_expr< array_exprt >(const exprt &base)

bool can_cast_expr< binary_exprt >(const exprt &base)

bool can_cast_expr< div_exprt >(const exprt &base)

const update_exprt & to_update_expr(const exprt &expr)

Cast an exprt to an update_exprt.

bool can_cast_expr< nil_exprt >(const exprt &base)

const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)

Cast an exprt to a unary_minus_exprt.

const equal_exprt & to_equal_expr(const exprt &expr)

Cast an exprt to an equal_exprt.

bool operator!=(const exprt &lhs, bool rhs)

Return whether the expression lhs is not a constant of Boolean type or is not representing the Boolea...

bool can_cast_expr< greater_than_or_equal_exprt >(const exprt &base)

bool can_cast_expr< implies_exprt >(const exprt &base)

bool can_cast_expr< unary_exprt >(const exprt &base)

bool can_cast_expr< less_than_or_equal_exprt >(const exprt &base)

const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)

Cast an exprt to a nondet_symbol_exprt.

bool can_cast_expr< union_exprt >(const exprt &base)

const member_designatort & to_member_designator(const exprt &expr)

Cast an exprt to an member_designatort.

bool can_cast_expr< complex_real_exprt >(const exprt &base)

const sign_exprt & to_sign_expr(const exprt &expr)

Cast an exprt to a sign_exprt.

const nor_exprt & to_nor_expr(const exprt &expr)

Cast an exprt to a nor_exprt.

const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)

Cast an exprt to a euclidean_mod_exprt.

const complex_typet & to_complex_type(const typet &type)

Cast a typet to a complex_typet.

size_t operator()(const ::symbol_exprt &sym)

const type_with_subtypet & to_type_with_subtype(const typet &type)

#define DATA_CHECK(vm, condition, message)

This macro takes a condition which denotes a well-formedness criterion on goto programs,...