ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
annotation_parser.h
Go to the documentation of this file.
1#pragma once
2
3#include <nlohmann/json.hpp>
4
5#include <string>
6
7// AST-walking helpers extracted from python_annotation.h. These are
8// pure functions over the JSON AST: they read the tree and return
9// found nodes (or an empty Json). They never mutate the AST and do
10// not depend on `python_annotation` class state.
12{
13// Find a top-level `Assign` whose target id is @p func_name and whose
14// value is a `Lambda`. Returns the surrounding `Assign` node, or an
15// empty Json when not found. Search is one level deep over @p body.
16nlohmann::json
17find_lambda_in_body(const std::string &func_name, const nlohmann::json &body);
18
19// Recursively walk @p body looking for a `FunctionDef` with the name
20// @p func_name. Descends into nested function bodies and the `body`
21// / `orelse` of any control-flow construct. Returns the matching
22// node or an empty Json.
23nlohmann::json find_function_recursive(
24 const std::string &func_name,
25 const nlohmann::json &body);
26
27// Inside class @p cls (looked up in @p ast_body), find the
28// `__init__` method and return the right-hand side of the first
29// `self.@p attr = ...` assignment. Returns an empty Json when no
30// such assignment exists. @p ast_body must be the top-level AST
31// `body` array (i.e. `ast["body"]`) — `json_utils::find_class`
32// iterates it expecting class-shaped nodes.
33nlohmann::json find_self_attr_init_rhs(
34 const std::string &cls,
35 const std::string &attr,
36 const nlohmann::json &ast_body);
37
38} // namespace python_annotation_parser
Definition annotation_parser.cpp:8
nlohmann::json find_function_recursive(const std::string &func_name, const nlohmann::json &body)
Definition annotation_parser.cpp:26
nlohmann::json find_self_attr_init_rhs(const std::string &cls, const std::string &attr, const nlohmann::json &ast_body)
Definition annotation_parser.cpp:66
nlohmann::json find_lambda_in_body(const std::string &func_name, const nlohmann::json &body)
Definition annotation_parser.cpp:10