ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
param_annotations.h
Go to the documentation of this file.
1#pragma once
2
3#include <nlohmann/json.hpp>
4#include <vector>
5
7{
12{
13 const nlohmann::json *read;
14 nlohmann::json *write;
15 std::string name;
16};
17
38void propagate_tuple_list_params(const std::vector<module_ast> &modules);
39
47void propagate_scalar_params(const std::vector<module_ast> &modules);
48} // namespace python_param_annotations
Definition param_annotations.cpp:1112
void propagate_scalar_params(const std::vector< module_ast > &modules)
Annotate the unannotated parameters of imported modules' top-level functions with the scalar type eve...
Definition param_annotations.cpp:1128
void propagate_tuple_list_params(const std::vector< module_ast > &modules)
Retype list[...] parameters from the tuples their callers pass.
Definition param_annotations.cpp:1113
One module's AST.
Definition param_annotations.h:12
nlohmann::json * write
Definition param_annotations.h:14
std::string name
Definition param_annotations.h:15
const nlohmann::json * read
Definition param_annotations.h:13