ACSLLogicType.cpp

                DefineGotoCase(TypeSuffix)
              } else {
                DefineAddErrorAndParse(
                  "unexpected 'double' type specification")
              }
            }
            default:
              DefineGotoCaseAndParse(TypeSuffix)
         }
        }
        else
          DefineGotoCaseAndParse(TypeSuffix)
    }
    DefineParseCase(TypeSuffix)
      { AbstractToken token = arguments.queryToken();
        if (!_doesStopSuffix
              && token.getType() == AbstractToken::TOperatorPunctuator) {
          OperatorPunctuatorToken::Type
              type = ((const OperatorPunctuatorToken&) token).getType();
          if (type == OperatorPunctuatorToken::TStar) {
            _typeResult = logic_type_Lpointer(_typeResult);
            arguments.extendLocationWithToken(_loc);
            DefineGotoCase(TypeSuffix)
          };
          if (type == OperatorPunctuatorToken::TAmpersand) {
            _typeResult = logic_type_Lreference(_typeResult);
            arguments.extendLocationWithToken(_loc);
            DefineGotoCase(TypeSuffix)
          };
          if (type == OperatorPunctuatorToken::TOpenBracket) {
            TermOrPredicate* subTerm = new TermOrPredicate;
            state.absorbRuleResult(&subTerm->setTerm());
            arguments.extendLocationWithToken(_loc);
            DefineShift(TypeSuffixArray, *subTerm, &TermOrPredicate::readToken)
          };
        }
        else if (token.getType() == AbstractToken::TKeyword) {
          KeywordToken::Type type = ((const KeywordToken&) token).getType();
          if (type == KeywordToken::TConst || type == KeywordToken::TVolatile) {
            arguments.extendLocationWithToken(_loc);
            DefineGotoCase(CTypeSuffix)
          };
        };
      }
      DefineReduceAndParse
    DefineParseCase(LogicTypeSuffix)
      { AbstractToken token = arguments.queryToken();
        if (!_doesStopSuffix
            && token.getType() == AbstractToken::TOperatorPunctuator) {
          OperatorPunctuatorToken::Type
            type = ((const OperatorPunctuatorToken&) token).getType();
          if (type == OperatorPunctuatorToken::TStar) {
            DefineAddError("pointers cannot point onto a logic type");
            _typeResult = logic_type_Lpointer(_typeResult);
            arguments.extendLocationWithToken(_loc);
            DefineGotoCase(LogicTypeSuffix)
          };
          if (type == OperatorPunctuatorToken::TAmpersand) {
            DefineAddError("references cannot reference a logic type");
            _typeResult = logic_type_Lreference(_typeResult);
            arguments.extendLocationWithToken(_loc);
            DefineGotoCase(LogicTypeSuffix)
          };
          if (type == OperatorPunctuatorToken::TOpenBracket) {
            TermOrPredicate* subTerm = new TermOrPredicate;
            state.absorbRuleResult(&subTerm->setTerm());
            arguments.extendLocationWithToken(_loc);
            DefineShift(TypeSuffixArray, *subTerm, &TermOrPredicate::readToken)
          };
        }
        else if (token.getType() == AbstractToken::TKeyword) {
          KeywordToken::Type type = ((const KeywordToken&) token).getType();
          if (type == KeywordToken::TConst || type == KeywordToken::TVolatile) {
            arguments.extendLocationWithToken(_loc);
            DefineGotoCase(LogicTypeSuffix)
          };
        };
      }
      DefineReduceAndParse
    DefineParseCase(TypeSuffixArray)
      { AbstractToken token = arguments.queryToken();
        if (token.getType() == AbstractToken::TOperatorPunctuator
            && (((const OperatorPunctuatorToken&) token).getType()
              == OperatorPunctuatorToken::TCloseBracket)) {
          // int intResult = 0; double doubleResult = 0;
          logic_type ltype = NULL;
          term termNode = NULL;
          std::string dimension = "0";
          // bool isRValue = false;
          { Parser::State::RuleAccess::TCastFromRule<TermOrPredicate>
              subterm(state.getRuleResult());
            // bool isConstant = false; // [TODO] activate it!
            termNode = subterm->extractTerm(arguments, ltype);
            state.freeRuleResult();
          };
          // if (!isRValue) {
          //   // term_lval_cons ...
          //   // term_node = term_node_TLval(lval)
          // };
          if (!ltype || !termNode) {
            if (arguments.doesStopAfterTooManyErrors())
              return RRFinished;
            DefineReduceAndParse
          };
          assert(false); // unimplemented
          _typeResult =
            logic_type_Larray(
              _typeResult,
              opt_some_container(logic_constant_LCInt(dimension.c_str())));
          DefineGotoCase(CTypeSuffix)
          DefineTReduce
        };
      };
      { std::ostringstream outToken;
        arguments.lexer().assumeContentToken();
        arguments.getContentToken().write(outToken,
            AbstractToken::PersistentFormat().setPretty());
        DefineAddError(std::string("unexpected token '")
            .append(outToken.str())
            .append("' when parsing the dimension of a cast "
              "with a logic array type"));
      };
      DefineGotoCase(TypeSuffixArray)
    DefineParseCase(TypeProduct)
      // TODO only the parsing rules are correct. Type products are not
      // implemented in the IR.
      { Parser::State::RuleAccess::TCastFromRule<LogicType>
            subtype(state.getRuleResult());
        // ...
        state.freeRuleResult();
        AbstractToken token = arguments.queryToken();
        if (token.getType() == AbstractToken::TOperatorPunctuator) {
          OperatorPunctuatorToken::Type type
              = ((const OperatorPunctuatorToken&) token).getType();
          if (type == OperatorPunctuatorToken::TCloseParen) {
            _typeResult = logic_type_Linteger();
            arguments.extendLocationWithToken(_loc);
            DefineGotoCase(LogicTypeSuffix)
          };
          if (type == OperatorPunctuatorToken::TComma) {
            state.absorbRuleResult(new LogicType);
            DefineGotoCase(TypeProduct)
          };
        };
        std::ostringstream outToken;
        arguments.lexer().assumeContentToken();
        arguments.getContentToken().write(outToken,
            AbstractToken::PersistentFormat().setPretty());
        DefineAddError(std::string("unexpected token '")
            .append(outToken.str())
            .append("' when parsing a product type"));
      };
      DefineReduceAndParse
    DefineParseCase(TypeRecord)
      //TODO only the parsing rules are correct. Records are not implemented
      //in the IR
      { Parser::State::RuleAccess::TCastFromRule<LogicType>
            subtype(state.getRuleResult());
        // ...
        state.freeRuleResult();
        if (arguments.queryToken().getType() == AbstractToken::TIdentifier) {
          //const std::string& identifier =
          //  ((const IdentifierToken&) arguments.getContentToken()).content();
          DefineGotoCase(TypeRecordItem)
        };
        DefineAddError("expecting identifier when parsing a record type");
      };
      DefineGotoCaseAndParse(TypeRecordItem)
    DefineParseCase(TypeRecordItem)
      { AbstractToken token = arguments.queryToken();
        token = arguments.queryToken();
        if (token.getType() == AbstractToken::TOperatorPunctuator) {
          OperatorPunctuatorToken::Type type
              = ((const OperatorPunctuatorToken&) token).getType();
          if (type == OperatorPunctuatorToken::TCloseBrace) {
            _typeResult = logic_type_Linteger();
            arguments.extendLocationWithToken(_loc);
            DefineGotoCase(LogicTypeSuffix)
          };
          if (type == OperatorPunctuatorToken::TSemiColon) {
            state.absorbRuleResult(new LogicType);
            DefineGotoCase(TypeProduct)
          };
        };
        std::ostringstream outToken;
        arguments.lexer().assumeContentToken();
        arguments.getContentToken().write(outToken,
            AbstractToken::PersistentFormat().setPretty());
        DefineAddError(std::string("unexpected token '")
            .append(outToken.str())
            .append("' when parsing a record type"));
      };
      DefineGotoCase(TypeRecordItem)
    DefineParseCase(TypeSumIdent)
      if (arguments.queryToken().getType() == AbstractToken::TIdentifier) {
        _sumIdentifier = ((const IdentifierToken&)
            arguments.getContentToken()).content();
        DefineGotoCase(EndTypeSum)
      };
      DefineAddError("expecting identifier when parsing a sum type");
      DefineGotoCaseAndParse(EndTypeSum)
    DefineParseCase(EndTypeSum)
      { assert(_superTypeName);
        bool is_extern_c = arguments.isExternCContext();
        /* logic_ctor_info */ list* endSum = &_typedefResult
            ->cons_logic_type_def.LTsum.arguments;
        while (*endSum)
          endSum = &(*endSum)->next;
        
        *endSum =
          cons_container(
            logic_ctor_info_cons(
              qualified_name_cons(NULL, strdup(_sumIdentifier.c_str())),
              is_extern_c,
              qualified_name_dup(_superTypeName), NULL), NULL);
        _sumIdentifier = "";
        AbstractToken token = arguments.queryToken();
        token = arguments.queryToken();
        if (token.getType() == AbstractToken::TOperatorPunctuator) {
          OperatorPunctuatorToken::Type type
            = ((const OperatorPunctuatorToken&) token).getType();
          if (type == OperatorPunctuatorToken::TOpenParen) {
            LogicType* rule = new LogicType;
            state.absorbRuleResult(rule);
            DefineShift(TypeConstructorParam, *rule, &LogicType::readToken);
          };
          if (type == OperatorPunctuatorToken::TBitOr)
            DefineGotoCase(TypeSumIdent)
        };
      };
      DefineReduceAndParse
    DefineParseCase(TypeConstructorParam)
      { Parser::State::RuleAccess::TCastFromRule<LogicType>
            definition(state.getRuleResult());
        /* logic_ctor_info */ list*
            endSum = &_typedefResult->cons_logic_type_def.LTsum.arguments;
        while (*endSum)
          endSum = &(*endSum)->next;
        /* logic_type */ list* locationParams =
            &((logic_ctor_info) (*endSum)->element.container)->ctor_params;
        while (*locationParams)
          locationParams = &(*locationParams)->next;
        (*locationParams) = cons_container(definition->extractType(), NULL);
        state.freeRuleResult();
        AbstractToken token = arguments.queryToken();
        if (token.getType() == AbstractToken::TOperatorPunctuator) {
          OperatorPunctuatorToken::Type
              type = ((const OperatorPunctuatorToken&) token).getType();
          if (type == OperatorPunctuatorToken::TComma) {
            LogicType* rule = new LogicType;
            state.absorbRuleResult(rule);
            DefineShift(TypeConstructorParam, *rule, &LogicType::readToken);
          };
          if (type == OperatorPunctuatorToken::TCloseParen)
            DefineGotoCase(EndTypeSum)
        };
      };
      DefineAddError("expecting ',' or ')' in the parameters of a sum type");
      DefineGotoCase(TypeConstructorParam)
  };
  return result;
}

std::string str(logic_type typ) {
  std::string n;
  tag_logic_type tag = typ->tag_logic_type;
  if (tag == LINTEGER) return "integer";
  if (tag == LREAL) return "real";
  if (tag == LINT) return "int#";
  if (tag == LFLOAT) {
    auto tagf = typ->cons_logic_type.Lfloat.kind;
    if (tagf == FDOUBLE) return "double";
    if (tagf == FFLOAT) return "float";
  }
  return  "????";
}

std::string str(list typs) {
  std::ostringstream s;
  while (typs) {
    logic_type curr_type =
            ((logic_arg_decl)typs->element.container)->la_type;
    s << str(curr_type) << " ";
    typs = typs->next;
  }
  return s.str();
}


#if defined(__clang__) || defined(__GNUC__)
#pragma GCC diagnostic pop
#endif

} // end of namespace Acsl