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

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

10#ifndef CPROVER_UTIL_STD_CODE_H

11#define CPROVER_UTIL_STD_CODE_H

13#include <list>

24{

25public:

42 {

43 return op0();

44 }

47 {

48 return op1();

49 }

52 {

53 return op0();

54 }

57 {

58 return op1();

59 }

62 const codet &code,

64 {

66 vm, code.operands().size() == 2, "assignment must have two operands");

67 }

70 const codet &code,

73 {

77 vm,

79 "lhs and rhs of assignment must have same type");

80 }

83 const codet &code,

86 {

88 {

90 }

93 }

95protected:

100};

101

102template <>

107

112

119

126

130{

131public:

135

137

142

147

149 {

152 s.reserve(_list.size());

153 for(const auto &c : _list)

154 s.push_back(c);

155 return result;

156 }

157

162

167

172

177

179 {

181 add(std::move(code));

182 }

183

185

186

191

193};

194

199

200

201

202

204{

206 return static_cast<const code_blockt &>(code);

207}

208

214

217{

218public:

222

224 {

225 return op0();

226 }

227

229 {

230 return op0();

231 }

232

233protected:

238};

239

240template <>

245

250

252{

256 return ret;

257}

258

260{

264 return ret;

265}

266

270{

271public:

275

277 {

278 return op0();

279 }

280

282 {

283 return op0();

284 }

285

286protected:

291};

292

293template <>

298

303

305{

309 return ret;

310}

311

313{

317 return ret;

318}

319

322{

323public:

327

328protected:

333};

334

339

340

341

347{

348public:

353

358

363

368

374 {

376 return {};

377 return {op1()};

378 }

379

385 {

387 {

389 }

390 else if(operands().size() < 2)

391 {

394 }

395 else

396 {

398 }

399 }

400

402 const codet &code,

404 {

405

407 vm,

409 "declaration must have one or more operands");

411 vm,

413 "declaring a non-symbol: " +

415 }

416};

417

418template <>

423

428

435

442

457

460{

461public:

469

477

479 {

480 return op0();

481 }

482

484 {

485 return op0();

486 }

487

489 {

490 return static_cast<const codet &>(op1());

491 }

492

497

499 {

500 return static_cast<const codet &>(op2());

501 }

502

504 {

505 return static_cast<codet &>(op1());

506 }

507

509 {

510 return static_cast<codet &>(op2());

511 }

512

513protected:

518};

519

524

529

531{

535 return ret;

536}

537

539{

543 return ret;

544}

545

548{

549public:

554

556 {

557 return op0();

558 }

559

561 {

562 return op0();

563 }

564

569

571 {

572 return static_cast<codet &>(op1());

573 }

574

575protected:

580};

581

586

591

593{

597 return ret;

598}

599

601{

605 return ret;

606}

607

610{

611public:

616

618 {

619 return op0();

620 }

621

623 {

624 return op0();

625 }

626

631

633 {

634 return static_cast<codet &>(op1());

635 }

636

637protected:

642};

643

648

653

655{

659 return ret;

660}

661

663{

667 return ret;

668}

669

672{

673public:

678

680 {

681 return op0();

682 }

683

685 {

686 return op0();

687 }

688

693

695 {

696 return static_cast<codet &>(op1());

697 }

698

699protected:

704};

705

710

715

717{

721 return ret;

722}

723

725{

729 return ret;

730}

731

734{

735public:

741 {std::move(_init),

742 std::move(_cond),

743 std::move(_iter),

744 std::move(_body)})

745 {

746 }

747

748

750 {

751 return op0();

752 }

753

755 {

756 return op0();

757 }

758

760 {

761 return op1();

762 }

763

765 {

766 return op1();

767 }

768

770 {

771 return op2();

772 }

773

775 {

776 return op2();

777 }

778

783

785 {

786 return static_cast<codet &>(op3());

787 }

788

805

806protected:

811};

812

817

822

824{

828 return ret;

829}

830

832{

836 return ret;

837}

838

841{

842public:

847

852

857

858protected:

863};

864

869

874

876{

880 return ret;

881}

882

884{

888 return ret;

889}

890

893{

894public:

898

902

904 {

905 return op0();

906 }

907

909 {

910 return op0();

911 }

912

917

919 const codet &code,

921 {

922 DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");

923 }

924

925protected:

930};

931

932template <>

937

942

949

956

959{

960public:

966

971

976

978 {

979 return static_cast<codet &>(op0());

980 }

981

983 {

984 return static_cast<const codet &>(op0());

985 }

986

987protected:

992};

993

998

1003

1005{

1009 return ret;

1010}

1011

1013{

1017 return ret;

1018}

1019

1023{

1024public:

1029

1034

1039

1041 {

1042 return op0();

1043 }

1044

1046 {

1047 return op0();

1048 }

1049

1051 {

1052 return static_cast<codet &>(op1());

1053 }

1054

1056 {

1057 return static_cast<const codet &>(op1());

1058 }

1059

1060protected:

1065};

1066

1071

1076

1078{

1082 return ret;

1083}

1084

1086{

1090 return ret;

1091}

1092

1097{

1098public:

1102 {std::move(_lower), std::move(_upper), std::move(_code)})

1103 {

1104 }

1105

1108 {

1109 return op0();

1110 }

1111

1114 {

1115 return op0();

1116 }

1117

1120 {

1121 return op1();

1122 }

1123

1126 {

1127 return op1();

1128 }

1129

1132 {

1133 return static_cast<codet &>(op2());

1134 }

1135

1138 {

1139 return static_cast<const codet &>(op2());

1140 }

1141

1142protected:

1147};

1148

1149template <>

1154

1156{

1157 validate_operands(x, 3, "gcc-switch-case-range must have three operands");

1158}

1159

1162{

1167 return ret;

1168}

1169

1171{

1176 return ret;

1177}

1178

1182{

1183public:

1187

1188protected:

1193};

1194

1199

1200

1201

1202

1204{

1206 return static_cast<const code_breakt &>(code);

1207}

1208

1210{

1212 return static_cast<code_breakt &>(code);

1213}

1214

1218{

1219public:

1223

1224protected:

1229};

1230

1235

1236

1237

1238

1244

1250

1253{

1254public:

1258

1262

1267

1272};

1273

1278

1279

1280

1281

1283{

1285 return static_cast<code_asmt &>(code);

1286}

1287

1289{

1291 return static_cast<const code_asmt &>(code);

1292}

1293

1297{

1298public:

1304

1306 {

1307 return op0();

1308 }

1309

1311 {

1312 return op0();

1313 }

1314

1316 {

1317 return op1();

1318 }

1319

1321 {

1322 return op1();

1323 }

1324

1326 {

1327 return op2();

1328 }

1329

1331 {

1332 return op2();

1333 }

1334

1336 {

1337 return op3();

1338 }

1339

1341 {

1342 return op3();

1343 }

1344

1349

1354

1355protected:

1360};

1361

1362template <>

1367

1372

1374{

1379 return ret;

1380}

1381

1383{

1388 return ret;

1389}

1390

1394{

1395public:

1400

1402 {

1403 return op0();

1404 }

1405

1407 {

1408 return op0();

1409 }

1410

1411protected:

1416};

1417

1422

1427

1429{

1433 return ret;

1434}

1435

1437{

1441 return ret;

1442}

1443

1450{

1451public:

1462

1471

1476

1481};

1482

1483namespace detail

1484{

1485

1486template<typename Tag>

1488{

1490 {

1491 return ptr->get_statement() == tag;

1492 }

1493 return false;

1494}

1495

1496}

1497

1502

1503

1504

1505

1511

1517

1520{

1521public:

1527

1532

1537};

1538

1539template<>

1544

1545

1546

1547

1554

1556 const exprt &expr)

1557{

1561}

1562

1565{

1566public:

1576

1585 {std::move(_lhs), std::move(_rhs)},

1586 std::move(_type),

1587 std::move(loc))

1588 {

1589 }

1590

1592 {

1593 return op0();

1594 }

1595

1597 {

1598 return op0();

1599 }

1600

1602 {

1603 return op1();

1604 }

1605

1607 {

1608 return op1();

1609 }

1610};

1611

1612template <>

1617

1624

1632

1635{

1636public:

1644 {std::move(_code)},

1645 std::move(_type),

1646 std::move(loc))

1647 {

1648 }

1649

1654

1659};

1660

1661template <>

1667

1678

1689

1692{

1693public:

1703 std::move(_type),

1704 std::move(loc))

1705 {

1706 }

1707

1709 {

1710 return op0();

1711 }

1712

1714 {

1715 return op0();

1716 }

1717

1722

1727};

1728

1729template<>

1734

1735

1736

1737

1745

1753

1757{

1758public:

1760 irept exception_list,

1764 {

1766 }

1767};

1768

1769template<>

1774

1775

1776

1777

1784

1786 const exprt &expr)

1787{

1791}

1792

1805{

1806public:

1811

1813 {

1814 public:

1818

1823

1829

1834

1838

1843

1847 };

1848

1850

1859

1863

1867

1868protected:

1873};

1874

1879

1880

1881

1882

1888

1894

1899{

1900public:

1904

1905protected:

1910};

1911

1916

1917

1918

1919

1925

1931

1936{

1937 public:

1942

1947

1949 {

1950 return op0();

1951 }

1953 {

1954 return op0();

1955 }

1956

1957protected:

1962};

1963

1968

1969

1970

1971

1977

1983

1986{

1987public:

1993

1995 {

1996 return static_cast<codet &>(op0());

1997 }

1998

2000 {

2001 return static_cast<const codet &>(op0());

2002 }

2003

2009

2015

2021

2027

2032

2033protected:

2038};

2039

2044

2046{

2047 validate_operands(x, 3, "try-catch must have three or more operands", true);

2048}

2049

2051{

2055 return ret;

2056}

2057

2059{

2063 return ret;

2064}

2065

2070{

2071public:

2073 const std::vector<irep_idt> &parameter_identifiers,

2076 {

2078 }

2079

2084

2089

2092

2093protected:

2098};

2099

2101{

2104 code.operands().size() == 1, "code_function_body must have one operand");

2106}

2107

2109{

2112 code.operands().size() == 1, "code_function_body must have one operand");

2114}

2115

2116#endif

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

codet representation of an inline assembler statement, for the gcc flavor.

const exprt & asm_text() const

const exprt & labels() const

const exprt & outputs() const

const exprt & inputs() const

const exprt & clobbers() const

codet representation of an inline assembler statement.

const irep_idt & get_flavor() const

void set_flavor(const irep_idt &f)

A non-fatal assertion, which checks a condition then permits execution to continue.

const exprt & assertion() const

An assumption, which must hold in subsequent code.

const exprt & assumption() const

A codet representing sequential composition of program statements.

static code_blockt from_list(const std::list< codet > &_list)

code_operandst & statements()

source_locationt end_location() const

void add(codet code, source_locationt loc)

code_blockt(std::vector< codet > &&_statements)

void append(const code_blockt &extra_block)

Add all the codets from extra_block to the current code_blockt.

code_blockt(const std::vector< codet > &_statements)

void add(const codet &code)

const code_operandst & statements() const

std::vector< codet > code_operandst

codet & find_last_statement()

codet representation of a break statement (within a for or while loop).

codet representation of a continue statement (within a for or while loop).

codet representation of a do while statement.

code_dowhilet(exprt _cond, codet _body)

const codet & body() const

const exprt & cond() const

codet representation of an expression statement.

code_expressiont(exprt expr)

const exprt & expression() const

codet representation of a for statement.

const exprt & cond() const

code_fort(exprt _init, exprt _cond, exprt _iter, codet _body)

A statement describing a for loop with initializer _init, loop condition _cond, increment _iter,...

static code_fort from_index_bounds(exprt start_index, exprt end_index, symbol_exprt loop_index, codet body, source_locationt location)

Produce a code_fort representing:

const exprt & iter() const

const codet & body() const

const exprt & init() const

A codet representing an assignment in the program.

static void validate(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)

static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)

code_frontend_assignt(exprt lhs, exprt rhs)

const exprt & lhs() const

const exprt & rhs() const

static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)

code_frontend_assignt(exprt lhs, exprt rhs, source_locationt loc)

A codet representing the declaration of a local variable.

code_frontend_declt(symbol_exprt symbol)

const symbol_exprt & symbol() const

void set_initial_value(std::optional< exprt > initial_value)

Sets the value to which this declaration initializes the declared variable.

std::optional< exprt > initial_value() const

Returns the initial value to which the declared variable is initialized, or empty in the case where n...

static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)

const irep_idt & get_identifier() const

codet representation of a "return from a function" statement.

const exprt & return_value() const

bool has_return_value() const

code_frontend_returnt(exprt _op)

static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)

This class is used to interface between a language frontend and goto-convert – it communicates the id...

code_function_bodyt(const std::vector< irep_idt > &parameter_identifiers, code_blockt _block)

std::vector< irep_idt > get_parameter_identifiers() const

const code_blockt & block() const

void set_parameter_identifiers(const std::vector< irep_idt > &)

codet representation of a switch-case, i.e. a case statement within a switch.

const codet & code() const

the statement to be executed when the case applies

const exprt & upper() const

upper bound of range

code_gcc_switch_case_ranget(exprt _lower, exprt _upper, codet _code)

const exprt & lower() const

lower bound of range

exprt & lower()

lower bound of range

exprt & upper()

upper bound of range

codet & code()

the statement to be executed when the case applies

codet representation of a goto statement.

const irep_idt & get_destination() const

code_gotot(const irep_idt &label)

void set_destination(const irep_idt &label)

codet representation of an if-then-else statement.

code_ifthenelset(exprt condition, codet then_code)

An if condition then then_code statement (no "else" case).

const exprt & cond() const

const codet & else_case() const

const codet & then_case() const

code_ifthenelset(exprt condition, codet then_code, codet else_code)

An if condition then then_code else else_code statement.

bool has_else_case() const

codet representation of a label for branch targets.

const irep_idt & get_label() const

code_labelt(const irep_idt &_label, codet _code)

const codet & code() const

void set_label(const irep_idt &label)

A statement that catches an exception, assigning the exception in flight to an expression (e....

const exprt & catch_expr() const

code_landingpadt(exprt catch_expr)

Pops an exception handler from the stack of active handlers (i.e.

void set_tag(const irep_idt &tag)

exception_list_entryt(const irep_idt &tag)

const irep_idt & get_label() const

exception_list_entryt(const irep_idt &tag, const irep_idt &label)

const irep_idt & get_tag() const

void set_label(const irep_idt &label)

Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....

exception_listt & exception_list()

std::vector< exception_list_entryt > exception_listt

const exception_listt & exception_list() const

code_push_catcht(const irep_idt &tag, const irep_idt &label)

A codet representing a skip statement.

codet representation of a switch-case, i.e. a case statement within a switch.

const exprt & case_op() const

code_switch_caset(exprt _case_op, codet _code)

const codet & code() const

codet representing a switch statement.

code_switcht(exprt _value, codet _body)

const codet & body() const

const exprt & value() const

codet representation of a try/catch block.

const code_frontend_declt & get_catch_decl(unsigned i) const

const codet & try_code() const

code_frontend_declt & get_catch_decl(unsigned i)

code_try_catcht(codet _try_code)

A statement representing try _try_code catch ...

void add_catch(code_frontend_declt &&to_catch, codet &&code_catch)

codet & get_catch_code(unsigned i)

const codet & get_catch_code(unsigned i) const

codet representing a while statement.

code_whilet(exprt _cond, codet _body)

const exprt & cond() const

const codet & body() const

Data structure for representing an arbitrary statement in a program.

const irep_idt & get_statement() const

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

Base class for all expressions.

std::vector< exprt > operandst

typet & type()

Return the type of the expression.

source_locationt & add_source_location()

void add_to_operands(const exprt &expr)

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

There are a large number of kinds of tree structured or tree-like data in CPROVER.

bool get_bool(const irep_idt &name) const

const irept & find(const irep_idt &name) const

const irep_idt & get(const irep_idt &name) const

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

const irep_idt & id() const

irept & add(const irep_idt &name)

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

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

A side_effect_exprt that performs an assignment.

const exprt & rhs() const

side_effect_expr_assignt(exprt _lhs, exprt _rhs, typet _type, source_locationt loc)

construct an assignment side-effect, given lhs, rhs and the type

const exprt & lhs() const

side_effect_expr_assignt(const exprt &_lhs, const exprt &_rhs, const source_locationt &loc)

construct an assignment side-effect, given lhs and rhs The type is copied from lhs

A side_effect_exprt representation of a function call side effect.

side_effect_expr_function_callt(exprt _function, exprt::operandst _arguments, typet _type, source_locationt loc)

const exprt::operandst & arguments() const

exprt::operandst & arguments()

const exprt & function() const

A side_effect_exprt that returns a non-deterministically chosen value.

void set_nullable(bool nullable)

bool get_nullable() const

side_effect_expr_nondett(typet _type, source_locationt loc)

A side_effect_exprt that contains a statement.

const codet & statement() const

side_effect_expr_statement_expressiont(codet _code, typet _type, source_locationt loc)

construct an assignment side-effect, given lhs, rhs and the type

A side_effect_exprt representation of a side effect that throws an exception.

side_effect_expr_throwt(irept exception_list, typet type, source_locationt loc)

An expression containing a side effect.

void set_statement(const irep_idt &statement)

const irep_idt & get_statement() const

side_effect_exprt(const irep_idt &statement, operandst _operands, typet _type, source_locationt loc)

side_effect_exprt(const irep_idt &statement, typet _type, source_locationt loc)

Expression to hold a symbol (variable)

const irep_idt & get_identifier() const

The type of an expression, extends irept.

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

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

bool can_cast_code_impl(const exprt &expr, const Tag &tag)

bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)

#define DATA_INVARIANT(CONDITION, REASON)

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

#define PRECONDITION(CONDITION)

side_effect_exprt & to_side_effect_expr(exprt &expr)

code_blockt create_fatal_assertion(const exprt &condition, const source_locationt &source_location)

Create a fatal assertion, which checks a condition and then halts if it does not hold.

bool can_cast_expr< side_effect_expr_throwt >(const exprt &base)

bool can_cast_expr< code_ifthenelset >(const exprt &base)

bool can_cast_expr< code_switcht >(const exprt &base)

const code_breakt & to_code_break(const codet &code)

const code_switch_caset & to_code_switch_case(const codet &code)

bool can_cast_expr< code_switch_caset >(const exprt &base)

bool can_cast_expr< code_asmt >(const exprt &base)

const code_function_bodyt & to_code_function_body(const codet &code)

bool can_cast_expr< code_expressiont >(const exprt &base)

bool can_cast_expr< code_landingpadt >(const exprt &base)

bool can_cast_expr< code_frontend_assignt >(const exprt &base)

const code_gotot & to_code_goto(const codet &code)

const code_assertt & to_code_assert(const codet &code)

bool can_cast_expr< code_blockt >(const exprt &base)

bool can_cast_expr< code_breakt >(const exprt &base)

bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)

bool can_cast_expr< code_dowhilet >(const exprt &base)

static code_push_catcht & to_code_push_catch(codet &code)

side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)

bool can_cast_expr< code_try_catcht >(const exprt &base)

bool can_cast_expr< code_frontend_returnt >(const exprt &base)

code_asm_gcct & to_code_asm_gcc(codet &code)

static code_landingpadt & to_code_landingpad(codet &code)

const code_frontend_returnt & to_code_frontend_return(const codet &code)

side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)

const code_dowhilet & to_code_dowhile(const codet &code)

static code_pop_catcht & to_code_pop_catch(codet &code)

side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)

const code_assumet & to_code_assume(const codet &code)

bool can_cast_expr< code_assertt >(const exprt &base)

const code_whilet & to_code_while(const codet &code)

bool can_cast_expr< code_skipt >(const exprt &base)

bool can_cast_expr< side_effect_expr_assignt >(const exprt &base)

bool can_cast_expr< code_asm_gcct >(const exprt &base)

bool can_cast_expr< code_frontend_declt >(const exprt &base)

bool can_cast_expr< code_gotot >(const exprt &base)

bool can_cast_expr< side_effect_expr_statement_expressiont >(const exprt &base)

const code_labelt & to_code_label(const codet &code)

bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)

const code_blockt & to_code_block(const codet &code)

const code_ifthenelset & to_code_ifthenelse(const codet &code)

const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)

void validate_expr(const code_frontend_assignt &x)

bool can_cast_expr< code_whilet >(const exprt &base)

bool can_cast_expr< code_continuet >(const exprt &base)

const code_frontend_assignt & to_code_frontend_assign(const codet &code)

bool can_cast_expr< side_effect_exprt >(const exprt &base)

code_asmt & to_code_asm(codet &code)

bool can_cast_expr< code_push_catcht >(const exprt &base)

side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)

const code_fort & to_code_for(const codet &code)

bool can_cast_expr< code_fort >(const exprt &base)

const code_switcht & to_code_switch(const codet &code)

const code_try_catcht & to_code_try_catch(const codet &code)

bool can_cast_expr< code_gcc_switch_case_ranget >(const exprt &base)

const code_frontend_declt & to_code_frontend_decl(const codet &code)

code_expressiont & to_code_expression(codet &code)

bool can_cast_expr< code_labelt >(const exprt &base)

bool can_cast_expr< code_pop_catcht >(const exprt &base)

side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)

const code_continuet & to_code_continue(const codet &code)

bool can_cast_expr< code_assumet >(const exprt &base)

const codet & to_code(const exprt &expr)

API to expression classes.

const symbol_exprt & to_symbol_expr(const exprt &expr)

Cast an exprt to a symbol_exprt.

#define DATA_CHECK(vm, condition, message)

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

void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)

Check that the given expression is well-formed (full check, including checks of all subexpressions an...