ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
literal_divergence.h File Reference
#include <nlohmann/json.hpp>
#include <string>
#include <unordered_map>
#include <unordered_set>
#include <utility>
#include <vector>
Include dependency graph for literal_divergence.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  dynamic_type_detail::numeric_bindingt

Namespaces

namespace  dynamic_type_detail

Functions

std::pair< std::string, std::string > dynamic_type_detail::callee_names (const nlohmann::json &func)
std::string dynamic_type_detail::scalar_name_kind (const std::string &type)
std::string dynamic_type_detail::nondet_leaf_kind (const std::string &leaf)
std::string dynamic_type_detail::constant_kind (const nlohmann::json &lit)
std::string dynamic_type_detail::classify_literal_value_kind (const nlohmann::json &value, const nlohmann::json &module_body=nlohmann::json())
bool & dynamic_type_detail::float_tags_possible ()
bool dynamic_type_detail::kinds_diverge (const std::unordered_set< std::string > &kinds)
std::string dynamic_type_detail::classify_name_kind (const std::string &name, const nlohmann::json &scope_body, const nlohmann::json &module_body=nlohmann::json())
std::string dynamic_type_detail::assigned_name (const nlohmann::json &target)
std::unordered_map< std::string, std::string > dynamic_type_detail::classify_branch_literal_assigns (const nlohmann::json &block, const nlohmann::json &scope_body, const nlohmann::json &module_body=nlohmann::json())
bool dynamic_type_detail::collect_branch_literal_kinds (const nlohmann::json &block, std::unordered_map< std::string, std::unordered_set< std::string > > &kinds, std::unordered_map< std::string, int > &leaf_count, int &leaf_total, const nlohmann::json &scope_body, const nlohmann::json &module_body=nlohmann::json())
bool dynamic_type_detail::collect_if_node_literal_kinds (const nlohmann::json &if_node, std::unordered_map< std::string, std::unordered_set< std::string > > &kinds, std::unordered_map< std::string, int > &leaf_count, int &leaf_total, const nlohmann::json &scope_body, const nlohmann::json &module_body=nlohmann::json())
bool dynamic_type_detail::assigns_name (const nlohmann::json &stmt, const std::string &name)
bool dynamic_type_detail::ifexp_arms_diverge (const nlohmann::json &value, const nlohmann::json &module_body)
bool dynamic_type_detail::scope_assigns_divergent_literal_types (const std::string &name, const nlohmann::json &scope_body, const nlohmann::json &module_body=nlohmann::json())
std::string dynamic_type_detail::numeric_binding_kind (const nlohmann::json &stmt, const std::string &name)
int dynamic_type_detail::line_field (const nlohmann::json &node, const char *key)
bool dynamic_type_detail::starts_after (const nlohmann::json &stmt, int before)
bool dynamic_type_detail::loop_spans (const nlohmann::json &stmt, int before)
void dynamic_type_detail::record_numeric_binding (const nlohmann::json &stmt, const std::string &name, bool nested, int before, std::vector< numeric_bindingt > &bindings)
void dynamic_type_detail::collect_numeric_bindings (const nlohmann::json &body, const std::string &name, bool nested, int before, bool include_later, std::vector< numeric_bindingt > &bindings)
bool dynamic_type_detail::is_path_dependent_number (const std::vector< numeric_bindingt > &bindings)