|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <nlohmann/json.hpp>#include <cstddef>Go to the source code of this file.
Classes | |
| struct | cmath_lowering_policy::expr_cost |
| struct | cmath_lowering_policy::budget |
Namespaces | |
| namespace | cmath_lowering_policy |
| Budget model that decides when cmath calls should be lowered inline vs dispatched to the Python model. | |
Functions | |
| expr_cost | cmath_lowering_policy::measure (const nlohmann::json &arg) |
| bool | cmath_lowering_policy::within_budget (const nlohmann::json &arg, const budget &b) |