- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <clang-c-frontend/clang_c_adjust.h>#include <clang-c-frontend/clang_c_adjust_guards.h>#include <clang-c-frontend/clang_c_adjust_irep2.h>#include <clang-c-frontend/padding.h>#include <clang-c-frontend/builtin_names.h>#include <clang-c-frontend/clang_c_base_layout.h>#include <util/irep/migrate.h>#include <util/lang/c_typecast.h>#include <util/lang/c_types.h>#include <irep2/irep2_utils.h>#include <util/config/config.h>#include <util/symtab/namespace.h>#include <util/symtab/pretty.h>#include <util/symtab/cprover_prefix.h>#include <optional>#include <utility>Macros | |
| #define | ARM(member) |
| Name and member from one token, so the string the ordering test matches on and the member it names cannot drift apart. | |
Functions | |
| static locationt | statement_location (const expr2tc &expr) |
| The source location of expr when it is a statement that can hold a call in a sub-expression, empty otherwise. | |
| static bool | is_width_suffixed (const std::string &name, const std::string &stem) |
| One of a family of spellings differing only by the argument's width: __builtin_popcount, ...l, ...ll and the type-generic ...g. | |
| static void | fold_comparison_builtin (const std::string &name, const expr2tc &l, const expr2tc &r, expr2tc &expr) |
| The ordered-comparison builtins, which differ from the plain operators only in being defined when an operand is NaN. | |
| static void | fold_unary_builtin (const std::string &name, const expr2tc &arg, expr2tc &expr) |
| The one-argument builtins that lower to a single IREP2 node. | |
| static bool | fold_pointer_intrinsic (const std::string &name, const std::vector< expr2tc > &args, expr2tc &expr) |
| The three pointer intrinsics do_special_functions matches by their __ESBMC_ name rather than a __builtin_ prefix. | |
| static bool | fold_float_constant (expr2tc &expr, const irep_idt &name, bool &handled) |
| The lowerings do_special_functions selects by base name rather than by a reserved __builtin_ prefix. | |
| static bool | lower_float_library_call (expr2tc &expr, const irep_idt &name, const std::vector< expr2tc > &args) |
| C17 7.12.10.2: remainder() is IEEE 754 remainder, exactly SMT-LIB's fp.rem. | |
| static bool | is_shift_assignment (const irep_idt &op) |
| The shift spellings clang_c_adjust returns early on: it promotes only the right operand there, which the corpus shows is already the migrated shape. | |
| static bool | binds_by_reference (const expr2tc &callee, const expr2tc &arg, const type2tc ¶m, std::size_t i, const contextt &context, const namespacet &ns, pointer_ref_kindt &rk) |
True when arg is bound to parameter i of callee rather than converted to its type – va_start(ap, n) hands the callee &ap. | |
| static bool | contains_sideeffect (const expr2tc &expr) |
| void | adjust_comma_at_dispatch (exprt &expr, const namespacet &ns) |
| Shape-2 probe (scope-clang-c-irep2.md §57): run the IREP2 comma rewrite at the point the legacy pass dispatches it, rather than in a second whole- program pass. | |
| #define ARM | ( | member | ) |
Name and member from one token, so the string the ordering test matches on and the member it names cannot drift apart.
| void adjust_comma_at_dispatch | ( | exprt & | expr, |
| const namespacet & | ns ) |
Shape-2 probe (scope-clang-c-irep2.md §57): run the IREP2 comma rewrite at the point the legacy pass dispatches it, rather than in a second whole- program pass.
§55.4 attributes the comma arm's divergences to that ordering alone; this is the experiment that decides it.
|
static |
True when arg is bound to parameter i of callee rather than converted to its type – va_start(ap, n) hands the callee &ap.
pointer_type2t has no field for the #reference bit clang_c_convertert::get_type sets, so migrate_type drops it and the rule c_typecastt::implicit_typecast_followed applies on the legacy path cannot be stated against the IREP2 types. It survives on the symbol's legacy typet, which is what this reads – the same route the implicit-callee arm above already takes to recover a base name. The rest of the conjunction is legacy's own precondition, kept whole so the two paths decide alike.
Whether a parameter is a reference is a property of the target, not of the callee's name: clang's A builtin-type code is an lvalue reference where __builtin_va_list is a pointer or a struct, and an already-decayed pointer where it is an array (x86-64 Linux). Reading the bit follows the target; a name test would take the address on both. rk receives the reference kind the legacy declaration spells, which the IREP2 parameter type need not carry – that asymmetry is why the check below reads the declaration at all.
|
static |
The ordered-comparison builtins, which differ from the plain operators only in being defined when an operand is NaN.
The lowerings do_special_functions selects by base name rather than by a reserved __builtin_ prefix.
Returns true when expr was rewritten.
sqrt's legacy arm additionally skips a py:-prefixed callee; this pass is constructed only from clang_c_languaget::typecheck, so no Python symbol can reach it and the guard has nothing to test. The argument-less float constants. handled distinguishes "not one of these" from "one of these, but declined".
|
static |
The three pointer intrinsics do_special_functions matches by their __ESBMC_ name rather than a __builtin_ prefix.
Each lowers to a node the backend evaluates in place; left as a call the symbol is bodyless and goto_check's "non-intrinsic prefixed with __ESBMC" rejects the program. Returns true when expr was rewritten.
The one-argument builtins that lower to a single IREP2 node.
The shift spellings clang_c_adjust returns early on: it promotes only the right operand there, which the corpus shows is already the migrated shape.
|
static |
One of a family of spellings differing only by the argument's width: __builtin_popcount, ...l, ...ll and the type-generic ...g.
The lowering is the same node for all of them, so the suffix carries no information here.
|
static |
C17 7.12.10.2: remainder() is IEEE 754 remainder, exactly SMT-LIB's fp.rem.
Lower only when the call is shaped like the C library function.
Legacy exempts the model build from the shape test, where its own remainder() calls are what put ieee_rem into the model. That is not ported: clang-c-irep2-adjust-only is not one of c2goto's options (src/c2goto/c2goto.cpp), so this pass never runs under building-c-library.
The source location of expr when it is a statement that can hold a call in a sub-expression, empty otherwise.
sideeffect2t carries none of its own, so a call in one takes the enclosing statement's – which is what clang_c_adjust reads off the side_effect_expr_function_callt it is handed (§130.3). Every kind whose operands can be an expression is listed: a condition is as much a call site as an assignment's right-hand side, and omitting one leaves the counterexample with no file and line 0.
1.15.0