ChenfengWei0 / esbmc

The efficient SMT-based bounded model checker
http://esbmc.org/
Other
0 stars 1 forks source link

Added more return type support and simple polymorphism support #1

Closed Sleepytt1210 closed 1 year ago

Sleepytt1210 commented 1 year ago

I've added more dynamic return type support for make_callexpr_return_type() method and make_pointee_type() method. Previously, it hard-coded to only find "returns (int8)". I used regex to capture the return type inside the brackets.

    std::smatch matches;
    std::regex e ("returns \\((\\w+)\\)");
    std::string typeString = sub_expr["typeString"].get<std::string>();
    if (std::regex_search(typeString, matches, e)) {
      auto j2 = nlohmann::json::parse(R"({
          "typeIdentifier": "t_)" + matches[1].str() + R"(",
          "typeString": ")" + matches[1].str() + R"("
        })"
      );
      adjusted_expr = j2;

Polymorphism support is also added by making the symbol id of a contract's method more unique. The method's contract's name and id are included in symbol.id to avoid name clashing. Corresponding test cases are also added.