ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
adjust_arm< Pass > Struct Template Reference

Phase 6 (C.3) IREP2-native adjuster for the C frontend. More...

#include <clang_c_adjust_irep2.h>

Public Attributes

const char * name
void(* run )(Pass &, expr2tc &)
bool(* when )(const expr2tc &)

Detailed Description

template<class Pass>
struct adjust_arm< Pass >

Phase 6 (C.3) IREP2-native adjuster for the C frontend.

The eventual replacement for clang_c_adjust, following the shape python_adjust established (docs/roadmap/scope-clang-c-irep2.md §6): an in-place recursive walk over expr2tc rather than the converter's out-parameter seam.

The walk reads each code symbol's IREP2 value, recurses, and writes the result back only when it changed something. That gate keeps an untouched body clear of the round-trip losses python_adjust documents (a bitfield's #bitfield flag, an explicit alignment attribute, the C qualifiers), which C headers are exactly the place to hit – and it exercises migrate_expr over every construct the C corpus contains either way, since symbolt::get_value2() migrates on demand and a construct that cannot migrate aborts here rather than much later.

The gate has a cost worth knowing about when reading a symbol-table A/B: an unchanged body still prints its converter tree, which is not what this pass produced. See writeback_all below and §135.

Known limitation: the walk aborts on a union constant whose type is still a by-name tag – migrate_expr hands migrate_type's symbol_type2t to constant_union2tc, whose is_union_type assertion then fires. Running after clang_c_adjust was meant to guarantee resolved aggregate types, as it does for Python after clang_cpp_adjust; for C it does not. 12 of the 1686 tests in regression/esbmc reach it. Left unguarded on purpose: this is the defect the walk exists to surface, and the flag is opt-in. One arm of an IREP2 adjust pass's dispatch: its name, the guard that decides whether it claims a node, and the rewrite it then applies. A null when is offered every node and guards itself.

Templated on the pass so a second frontend can order the arms it inherits alongside its own in one table. run is a trampoline rather than a pointer-to-member deliberately: a base member pointer stored in a derived-typed table is legal, but GCC 13's array-bounds analysis mis-reads the call once the runner inlines and rejects it at -O2 (docs/roadmap/scope-clang-cpp-irep2.md §3.1). A captureless lambda converts to a function pointer and is an address constant, so the table stays constant-initialised.

Member Data Documentation

◆ name

template<class Pass>
const char* adjust_arm< Pass >::name

◆ run

template<class Pass>
void(* adjust_arm< Pass >::run) (Pass &, expr2tc &)

◆ when

template<class Pass>
bool(* adjust_arm< Pass >::when) (const expr2tc &)

The documentation for this struct was generated from the following file: