cprover
|
Expressions in JSON. More...
#include "json_expr.h"
#include "namespace.h"
#include "expr.h"
#include "json.h"
#include "arith_tools.h"
#include "ieee_float.h"
#include "fixedbv.h"
#include "std_expr.h"
#include "config.h"
#include "identifier.h"
#include "invariant.h"
#include <langapi/mode.h>
#include <langapi/language.h>
#include <memory>
Go to the source code of this file.
Functions | |
static exprt | simplify_json_expr (const exprt &src, const namespacet &ns) |
json_objectt | json (const source_locationt &location) |
json_objectt | json (const typet &type, const namespacet &ns, const irep_idt &mode) |
Output a CBMC type in json. More... | |
json_objectt | json (const exprt &expr, const namespacet &ns, const irep_idt &mode) |
Output a CBMC expression in json. More... | |
Expressions in JSON.
Definition in file json_expr.cpp.
json_objectt json | ( | const source_locationt & | location | ) |
Definition at line 83 of file json_expr.cpp.
References dstringt::empty(), source_locationt::get_column(), source_locationt::get_file(), source_locationt::get_function(), source_locationt::get_java_bytecode_index(), source_locationt::get_line(), and source_locationt::get_working_directory().
Referenced by add_to_json(), show_goto_functions_jsont::convert(), convert(), convert_decl(), goto_difft::convert_function_json(), convert_input(), convert_output(), convert_properties_json(), convert_return(), json(), ui_message_handlert::json_ui_msg(), taint_analysist::operator()(), bmc_covert::operator()(), ai_domain_baset::output_json(), dep_graph_domaint::output_json(), json_stream_arrayt::push_back(), json_arrayt::push_back(), reachable_functions(), show_loop_ids_json(), bmct::show_vcc_json(), static_verifier(), taint_parser(), unreachable_functions(), and unreachable_instructions().
json_objectt json | ( | const typet & | type, |
const namespacet & | ns, | ||
const irep_idt & | mode | ||
) |
Output a CBMC type in json.
The mode
argument is used to correctly report types.
type | a type |
ns | a namespace |
mode | language in which the code was written; for now ID_C and ID_java are supported |
Definition at line 115 of file json_expr.cpp.
References struct_union_typet::components(), namespace_baset::follow(), namespace_baset::follow_tag(), irept::id(), json(), jsont::make_array(), jsont::make_object(), json_arrayt::push_back(), typet::subtype(), to_bv_type(), to_c_bit_field_type(), to_c_enum_tag_type(), to_fixedbv_type(), to_floatbv_type(), to_signedbv_type(), to_string(), to_struct_type(), to_union_type(), to_unsignedbv_type(), and to_vector_type().
json_objectt json | ( | const exprt & | expr, |
const namespacet & | ns, | ||
const irep_idt & | mode | ||
) |
Output a CBMC expression in json.
The mode is used to correctly report types.
expr | an expression |
ns | a namespace |
mode | language in which the code was written; for now ID_C and ID_java are supported |
Definition at line 224 of file json_expr.cpp.
References CHECK_RETURN, identifiert::components, struct_union_typet::components(), DATA_INVARIANT, namespace_baset::follow(), namespace_baset::follow_tag(), forall_operands, languaget::from_expr(), languaget::from_type(), irept::get(), union_exprt::get_component_name(), get_default_language(), symbol_exprt::get_identifier(), get_language_from_mode(), irept::get_string(), constant_exprt::get_value(), bitvector_typet::get_width(), irept::id(), id2string(), exprt::is_true(), json(), jsont::json_boolean(), jsont::make_array(), jsont::make_object(), unary_exprt::op(), exprt::op0(), exprt::operands(), json_arrayt::push_back(), constant_exprt::set_value(), simplify_json_expr(), typet::subtype(), to_bitvector_type(), to_c_enum_tag_type(), to_constant_expr(), to_string(), to_struct_type(), to_symbol_expr(), to_union_expr(), and exprt::type().
|
static |
Definition at line 30 of file json_expr.cpp.
References configt::ansi_c, config, namespace_baset::follow(), constant_exprt::get_value(), irept::id(), id2string(), configt::ansi_ct::NULL_is_zero, exprt::op0(), exprt::operands(), dstringt::size(), to_constant_expr(), to_index_expr(), to_member_expr(), and exprt::type().
Referenced by json().