Mapping type conversion for the Solidity frontend. More...

#include <solidity-frontend/solidity_convert.h>
#include <solidity-frontend/typecast.h>
#include <util/arith/arith_tools.h>
#include <util/arith/bitvector.h>
#include <util/lang/c_types.h>
#include <util/expr/expr_util.h>
#include <util/base/i2string.h>
#include <util/arith/mp_arith.h>
#include <util/irep/std_expr.h>
#include <util/message/message.h>
#include <fstream>

Include dependency graph for solidity_convert_mapping.cpp:

Detailed Description

Mapping type conversion for the Solidity frontend.

Converts Solidity mapping types into ESBMC's representation using infinite arrays (modeled as arrays with nondet size). Handles nested mappings, mapping access expressions, and the generation of helper symbols for mapping state variables.