Skip to content
Snippets Groups Projects
Forked from pub / Frama Clang
541 commits behind the upstream repository.
ACSLLogicType.cpp 53.21 KiB
/**************************************************************************/
/*                                                                        */
/*  This file is part of Frama-Clang                                      */
/*                                                                        */
/*  Copyright (C) 2012-2020                                               */
/*    CEA (Commissariat à l'énergie atomique et aux énergies              */
/*         alternatives)                                                  */
/*                                                                        */
/*  you can redistribute it and/or modify it under the terms of the GNU   */
/*  Lesser General Public License as published by the Free Software       */
/*  Foundation, version 2.1.                                              */
/*                                                                        */
/*  It is distributed in the hope that it will be useful,                 */
/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
/*  GNU Lesser General Public License for more details.                   */
/*                                                                        */
/*  See the GNU Lesser General Public License version 2.1                 */
/*  for more details (enclosed in the file LICENSE).                      */
/*                                                                        */
/**************************************************************************/

//
// Description:
//   Implementation of the ACSL logic types.
//

#include "ACSLTermOrPredicate.h"
#include "ACSLParser.h"

namespace Acsl {

bool is_signed(ikind i, Parser::Arguments &context) {
  switch (i) {
    case IBOOL:
    case ICHAR_U:
    case IUCHAR:
    case IWCHAR_U:
    case IWUCHAR:
    case IUSHORT:
    case IUINT:
    case IULONG:
    case ICHAR16:
    case ICHAR32:
      return false;
    case ICHAR:
      return context.is_char_signed();
    case IWCHAR:
      return context.is_wchar_signed();
    default:
      return true;
  }
}

bool equivalent_int_kind(ikind i1, ikind i2, Parser::Arguments &context) {
  if (i1 == i2) return true;
  if (is_signed(i1,context) != is_signed(i2,context)) return false;
  if ((i1 == IWCHAR || i1 == IWCHAR_U || i1 == IWCHAR_S) &&
      (i2 == IWCHAR || i2 == IWCHAR_U || i2 == IWCHAR_S)) return true;
  if ((i1 == ICHAR || i1 == ICHAR_U || i1 == ICHAR_S) &&
      (i2 == ICHAR || i2 == ICHAR_U || i2 == ICHAR_S)) return true;
  return false;
}

bool compatible_int_kind(ikind i1, ikind i2, Parser::Arguments &context) {
  if (equivalent_int_kind(i1,i2,context)) return true;
  if (i1 >= ISHORT && i2 < ISHORT)
    // char and bool are compatible with anything longer than short
    return true;
  if (is_signed(i1, context) != is_signed(i2, context)) return false;

  if (i1 == IULONG || i1 == ILONG) return true;
  if (i2 == IULONG || i2 == ILONG) return false;
  if (i1 == IUINT || i1 == IINT) return true;
  if (i2 == IUINT || i2 == IINT) return false;
  if (i1 == ISHORT || i1 == IUSHORT) return true;
  if (i2 == ISHORT || i2 == IUSHORT) return false;
  if (i1 == ICHAR || i1 == IUCHAR || i1 == ISCHAR) return true;
  // i1 is bool, i2 is not compatible with it
  return false;
}

bool compatible_float_kind(fkind f1, fkind f2) {
  if (f1 == FLONGDOUBLE) return true;
  if (f2 == FLONGDOUBLE) return false;
  if (f1 == FDOUBLE) return true;
  if (f2 == FDOUBLE) return false;
  // f1 == f2 == FFLOAT
  return true;
}

// true if v2 is compatible with v1, i.e. is a subtype of v1
// note that we don't use inheritance relation here to check for
// compatibility.
bool
logic_type_compatible(logic_type v1, logic_type v2,
                      Parser::Arguments &context) {
  while (v1->tag_logic_type == LREFERENCE)
    v1 = v1->cons_logic_type.Lreference.subtype;
  while (v2->tag_logic_type == LREFERENCE)
    v2 = v2->cons_logic_type.Lreference.subtype;
  tag_logic_type first = v1->tag_logic_type;
  tag_logic_type second = v2->tag_logic_type;

  // VP: technically, any int is compatible with a real, the test below
  // should be improved...
  if (first == LINT)
    first = LINTEGER;
  else if (first == LFLOAT)
    first = LREAL;
  if (second == LINT)
    second = LINTEGER;
  else if (second == LFLOAT)
    second = LREAL;

  if (second == LPOINTER && first == LARRAY) {
    v2 = v2->cons_logic_type.Lpointer.subtype;
    v1 = v1->cons_logic_type.Larray.subtype;
    first = v1->tag_logic_type;
    second = v2->tag_logic_type;
  };
  if (first == LENUM && second != LENUM)
    first = LINTEGER;

  if (first == LREAL && second == LINTEGER) second = LREAL;

  if (first != second)
    return false;
  switch (v1->tag_logic_type) {
    case LVOID:
      return true;
    case LINTEGER:
      return true;
    case LREAL:
      return true;
    case LINT: {
      if (v2->tag_logic_type == LINT) {
        return
          compatible_int_kind(
            v1->cons_logic_type.Lint.kind,
            v2->cons_logic_type.Lint.kind,
            context);
          }
      return false; // v2 is a LINTEGER
    }
    case LFLOAT: {
      if (v2->tag_logic_type == LFLOAT) {
        return
          compatible_float_kind(
            v1->cons_logic_type.Lfloat.kind, v2->cons_logic_type.Lfloat.kind);
      }
      return false; // v2 is a LREAL
    }
    case LARRAY:
      if (!logic_type_compatible(
            v1->cons_logic_type.Larray.subtype,
            v2->cons_logic_type.Larray.subtype,
            context))
        return false;
      if (v1->cons_logic_type.Larray.dim->is_some
          != v2->cons_logic_type.Larray.dim->is_some) {
        if (v2->cons_logic_type.Larray.dim->is_some)
          return false;
      }
      if (v1->cons_logic_type.Larray.dim->is_some) {
        if (!logic_constant_equal((logic_constant) v1->cons_logic_type
              .Larray.dim->content.container,
            (logic_constant)v2->cons_logic_type.Larray.dim->content.container))
          return false;
      };
      return true;
    case LPOINTER:
      return logic_type_compatible(
        v1->cons_logic_type.Lpointer.subtype,
        v2->cons_logic_type.Lpointer.subtype,
        context);
    case LENUM:
      return qualified_name_equal(v1->cons_logic_type.Lenum.name,
            v2->cons_logic_type.Lenum.name);
    case LSTRUCT:
      return qualified_name_equal(v1->cons_logic_type.Lstruct.name,
          v2->cons_logic_type.Lstruct.name)
        && tkind_equal(v1->cons_logic_type.Lstruct.template_kind,
          v2->cons_logic_type.Lstruct.template_kind);
    case LUNION:
      return qualified_name_equal(v1->cons_logic_type.Lunion.name,
          v2->cons_logic_type.Lunion.name)
        && tkind_equal(v1->cons_logic_type.Lunion.template_kind,
          v2->cons_logic_type.Lunion.template_kind);
    case LCNAMED:
      return qualified_name_equal(v1->cons_logic_type.LCnamed.name,
          v2->cons_logic_type.LCnamed.name);
    case LVARIABLE:
      return qualified_name_equal(v1->cons_logic_type.Lvariable.name,
          v2->cons_logic_type.Lvariable.name);
    case LNAMED:
      if (!qualified_name_equal(v1->cons_logic_type.Lnamed.name,
            v2->cons_logic_type.Lnamed.name))
        return false;
      { list l1 = v1->cons_logic_type.Lnamed.template_arguments,
             l2 = v2->cons_logic_type.Lnamed.template_arguments;
        while (l1 != NULL || l2 != NULL) {
          if (l1 == NULL || l2 == NULL)
            return false;
          if (!logic_type_equal((logic_type)l1->element.container,
                (logic_type)l2->element.container))
            return false;
          l1 = l1 -> next;
          l2 = l2 -> next;
        }
      }
      return true;
    case LARROW:
      { list l1 = v1->cons_logic_type.Larrow.left,
             l2 = v2->cons_logic_type.Larrow.left;
        while (l1 != NULL || l2 != NULL) {
          if (l1 == NULL || l2 == NULL)
            return false;
          if (!logic_type_compatible(
                (logic_type)l1->element.container,
                (logic_type)l2->element.container,
                context))
            return false;
          l1 = l1 -> next;
          l2 = l2 -> next;
        }
      }
      return logic_type_compatible(
        v1->cons_logic_type.Larrow.right,
        v2->cons_logic_type.Larrow.right,
        context);
    default:
      return false;
  }
  return false;
}

using namespace DLexer;

#if defined(__clang__) || defined(__GNUC__)
#pragma GCC diagnostic push
#pragma GCC diagnostic ignored "-Wunused-label"
#endif

bool is_type_synonym(logic_type_info info) {
  option def = info->definition;
  return
    def->is_some &&
    ((logic_type_def)def->content.container)->tag_logic_type_def == LTSYN;
}

logic_type make_set_type(logic_type base_type) {
  return
    logic_type_Lnamed(
      qualified_name_cons(NULL,strdup("set")),true,
      cons_container(base_type,NULL));
}

logic_type remove_set_type(logic_type set_type) {
  assert(TermOrPredicate::isSetType(set_type));
  return
    (logic_type)
    set_type->cons_logic_type.Lnamed.template_arguments->element.container;
}

// Extract a definition. is_type_synonym(info) must be true.
logic_type extract_synonym_def(logic_type_info info) {
  option def = info -> definition;
  assert(def->is_some);
  logic_type_def ltdef = (logic_type_def)def->content.container;
  assert(ltdef->tag_logic_type_def == LTSYN);
  return ltdef->cons_logic_type_def.LTsyn.def;
}

logic_type from_c_named_type(
  const clang::NamedDecl* type, const Clang_utils* utils) {
  clang::Decl::Kind kind = type->getKind();
  assert (kind >= clang::Decl::firstType && kind <= clang::Decl::lastType);
  if (kind >= clang::Decl::firstTypedefName && 
      kind <= clang::Decl::lastTypedefName) {
    const clang::TypedefNameDecl* tidentifier =
      static_cast<const clang::TypedefNameDecl*>(type);
    return
      logic_type_LCnamed(
        utils-> makeQualifiedName(*tidentifier),
        utils->isExternCContext(tidentifier->getDeclContext()));
  } else {
    return
      utils->makeLogicType(
        type->getLocation(),
        static_cast<const clang::TypeDecl*>(type)->getTypeForDecl());
  }
}

Parser::ReadResult
LogicType::readToken(Parser::State& state, Parser::Arguments& arguments) {
  enum Delimiters
    { DBegin, DAfterLogicIdentifier, DAfterLogicAndCContextIdentifier,
      DAfterQualifiedLogicIdentifier, DAfterQualifiedLogicAndCContextIdentifier,
      DAfterCContextIdentifier, DAfterQualifiedCContextIdentifier,
      DCTypeSignedSuffix, DCTypeUnsignedSuffix, DCTypeSuffix, DTypeSuffix,
      DLogicTypeSuffix, DTypeSuffixArray,
      DTypeProduct, DTypeRecord, DTypeRecordItem, DTypeSumIdent, DEndTypeSum,
      DTypeConstructorParam
    };

  ReadResult result = RRNeedChars;
  switch (state.point()) {
    DefineParseCase(Begin)
      { AbstractToken token = arguments.queryToken();
        if (!_loc)
          absorbLoc(arguments.newTokenLocation());
        KeywordToken::Type prefixedToken = KeywordToken::TUndefined;
        if (token.getType() == AbstractToken::TKeyword) {
          KeywordToken::Type kw = ((const KeywordToken&) token).getType();
          if (kw == KeywordToken::TStruct || kw == KeywordToken::TClass || kw == KeywordToken::TUnion) {
            // A struct/union/class keyword at the beginning of a type is permitted but not necessary.
            // So we skip it if the next token is an identifier
            prefixedToken = kw;
            result = arguments.lexer().readToken();
            if (result == RRFinished) {
              DefineAddError("unexpected end of input after a struct/union/class token, beginning a type");
              return result;
            }
            token = arguments.queryToken();
            if (!_loc) absorbLoc(arguments.newTokenLocation());
            if (token.getType() != AbstractToken::TIdentifier) {
              DefineAddError("expected an identifier after the struct, union, or class token at the beginning of a type");
              return RRFinished;
            }
          }
        }
        switch (token.getType()) {
          case AbstractToken::TIdentifier:
            { std::string identifier = ((const IdentifierToken&)
                arguments.getContentToken()).content();

              bool hasFoundLogicQualification = false;
              arguments.extendLocationWithToken(_loc);
              if ((_qualification = arguments.findLogicName(identifier))
                  != NULL) {
                if (_qualification->ssons())
                  hasFoundLogicQualification = true;
              };
              const clang::TemplateArgument* templateArgument=NULL;
              const clang::NamedDecl* cidentifier
                  = arguments.isCodeName(identifier, &templateArgument);
              if (cidentifier) {
                clang::Decl::Kind kind = cidentifier->getKind();
                if (kind >= clang::Decl::firstRecord
                      && kind <= clang::Decl::lastRecord) {
                  const clang::RecordDecl* decl =
                    llvm::dyn_cast<clang::RecordDecl>(cidentifier);
                  assert(decl);
                  _declContext = decl;
                  switch (prefixedToken) {
                    case KeywordToken::TUndefined: break;
                    case KeywordToken::TUnion:
                      if (!decl->isUnion()) {
                        DefineAddError(identifier + " is not an union.");
                        return RRFinished;
                      }
                      break;
                    case KeywordToken::TStruct:
                    case KeywordToken::TClass:
                      if (!(decl->isStruct() || decl->isClass())) {
                        DefineAddError(
                          identifier + " is not a struct or class.");
                        return RRFinished;
                      }
                      break;
                    default: break;
                  }

                  if (!hasFoundLogicQualification)
                    DefineGotoCase(AfterCContextIdentifier)
                  else
                    DefineGotoCase(AfterLogicAndCContextIdentifier)
                };
                if (kind >= clang::Decl::firstType
                      && kind <= clang::Decl::lastType) {
                  if (prefixedToken != KeywordToken::TUndefined) {
                    DefineAddError(
                      identifier + " is not a struct, class, or union.");
                    return RRFinished;
                  }
                  if (hasFoundLogicQualification) /* else issue a conflict */
                    DefineGotoCase(AfterLogicIdentifier);
                  _typeResult =
                    from_c_named_type(cidentifier,arguments.get_clang_utils());
                  DefineGotoCase(TypeSuffix)
                };
                if ((kind >= clang::Decl::firstTemplate
                      && kind <= clang::Decl::lastTemplate)
                    || kind == clang::Decl::NonTypeTemplateParm) {
                  DefineAddError(
                    "unsupported: templates in logic annotations");
                  return RRFinished;
                  // the following is completely false: we have Foo<Bar> in
                  // ACSL++ and translate it as Bar in IR...
                  // assert(templateArgument);
                  // switch (templateArgument->getKind()) {
                  //  case clang::TemplateArgument::Type:
                  //    _typeResult =
                  //      arguments.get_clang_utils()->makeLogicType(
                  //        arguments.tokenSourceLocation(),
                  //        templateArgument->getAsType().getTypePtr());
                  //    DefineGotoCase(TypeSuffix)
                  //  default:
                  //    break;
                  // };
                };
                if (prefixedToken != KeywordToken::TUndefined) {
                  DefineAddError(
                    identifier + " is a namespace.");
                  return RRFinished;
                }
                switch (kind) {
                  // case clang::Decl::Label:
                  case clang::Decl::Namespace:
                    assert(llvm::dyn_cast<clang::NamespaceDecl>(cidentifier));
                    _declContext = static_cast<const clang::NamespaceDecl*>(
                        cidentifier);
                    if (!hasFoundLogicQualification)
                      DefineGotoCase(AfterCContextIdentifier)
                    else
                      DefineGotoCase(AfterLogicAndCContextIdentifier)
                  case clang::Decl::NamespaceAlias:
                    assert(llvm::dyn_cast<clang::NamespaceAliasDecl>(
                          cidentifier));
                    _declContext = static_cast<const clang::NamespaceAliasDecl*>
                      (cidentifier)->getNamespace();
                    if (!hasFoundLogicQualification)
                      DefineGotoCase(AfterCContextIdentifier)
                    else
                      DefineGotoCase(AfterLogicAndCContextIdentifier);
                  default:
                    break;
                };
              };
              if (hasFoundLogicQualification)
                DefineGotoCase(AfterLogicIdentifier);
              if (_qualification) {
                if (_qualification->isLogicType()) {
                  logic_type_info ti =
                    _qualification->asLogicType().type_info();
                  _typeResult =
                    logic_type_Lnamed(
                      qualified_name_dup(ti->type_name), ti->is_extern_c, NULL);
                  DefineGotoCase(LogicTypeSuffix)
                };
                DefineGotoCase(AfterLogicIdentifier)
              };
              _typeResult = logic_type_Linteger();
              DefineAddError(std::string("unknown identifier '")
                  .append(identifier).append("'"));
              DefineReduce
            };
            break;
          case AbstractToken::TKeyword:
            switch (((const KeywordToken&) token).getType()) {
              case KeywordToken::TBool:
                _typeResult = logic_type_Lint(IBOOL);
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(TypeSuffix)
              case KeywordToken::TChar:
                _typeResult = logic_type_Lint(ICHAR);
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(CTypeSuffix)
              case KeywordToken::TChar16:
                _typeResult = logic_type_Lint(ICHAR16);
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(CTypeSuffix)
              case KeywordToken::TChar32:
                _typeResult = logic_type_Lint(ICHAR32);
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(CTypeSuffix);
              case KeywordToken::TConst:
              case KeywordToken::TVolatile:
                // don't know how to translate this in logic_type _typeResult
                DefineGotoCase(Begin)
              case KeywordToken::TDouble:
                _typeResult = logic_type_Lfloat(FDOUBLE);
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(CTypeSuffix)
              case KeywordToken::TFloat:
                _typeResult = logic_type_Lfloat(FFLOAT);
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(TypeSuffix)
              case KeywordToken::TInt:
                _typeResult = logic_type_Lint(IINT);
                _seenInt = true;
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(CTypeSuffix)
              case KeywordToken::TLong:
                _typeResult = logic_type_Lint(ILONG);
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(CTypeSuffix)
              case KeywordToken::TShort:
                _typeResult = logic_type_Lint(ISHORT);
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(CTypeSuffix)
              case KeywordToken::TSigned:
                _typeResult = logic_type_Lint(IINT);
                _seenSigned = true;
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(CTypeSuffix)
              case KeywordToken::TUnsigned:
                _typeResult = logic_type_Lint(IUINT);
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(CTypeSuffix)
              case KeywordToken::TVoid:
                _typeResult = logic_type_Lvoid();
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(TypeSuffix)
              case KeywordToken::TInteger:
                _typeResult = logic_type_Linteger();
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(LogicTypeSuffix)
              case KeywordToken::TReal:
                _typeResult = logic_type_Lreal();
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(LogicTypeSuffix)
              case KeywordToken::TBoolean:
                _typeResult = arguments.boolean_type();
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(LogicTypeSuffix)
              case KeywordToken::TWcharT:
                _typeResult = logic_type_Lint(IWCHAR);
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(CTypeSuffix)
              default:
                break;
            };
            { std::ostringstream outToken;
              arguments.lexer().assumeContentToken();
              arguments.getContentToken().write(outToken,
                  AbstractToken::PersistentFormat().setPretty());
              DefineAddError(std::string("keyword '")
                  .append(outToken.str())
                  .append("' encountered when parsing a type"));
            };
            DefineReduce
          case AbstractToken::TOperatorPunctuator:
            { OperatorPunctuatorToken::Type type
                = ((const OperatorPunctuatorToken&) token).getType();
              switch (type) {
                case OperatorPunctuatorToken::TOpenParen:
                  DefineAddError("product type is not implemented");
                  { LogicType* rule = new LogicType;
                    state.absorbRuleResult(rule);
                    DefineShift(TypeProduct, *rule, &LogicType::readToken);
                  };
                case OperatorPunctuatorToken::TOpenBrace:
                  DefineAddError("record type is not implemented");
                  { LogicType* rule = new LogicType;
                    state.absorbRuleResult(rule);
                    DefineShift(TypeRecord, *rule, &LogicType::readToken);
                  };
                case OperatorPunctuatorToken::TBitOr:
                  if (_superTypeName) {
                    _typedefResult = logic_type_def_LTsum(NULL);
                    DefineGotoCase(TypeSumIdent);
                  };
                default:
                  break;
              };
            };
          default:
            break;
        };
        { 
          arguments.lexer().assumeContentToken();
          DefineAddError(std::string("unexpected token '")
                    .append(arguments.getContentToken().str())
                    .append("' when starting to parse a type"));
        };
        DefineReduce;
      };
    DefineParseCase(AfterLogicIdentifier)
      { AbstractToken token = arguments.queryToken();
        if (token.getType() == AbstractToken::TOperatorPunctuator) {
          if (((const OperatorPunctuatorToken&) token).getType()
              == OperatorPunctuatorToken::TColonColon) {
            if (_qualification && !_qualification->ssons()) {
              std::string errorMessage = "unknown logic qualification ";
              errorMessage.append(_qualification->getName());
              DefineAddError(errorMessage)
            };
            DefineGotoCase(AfterQualifiedLogicIdentifier)
          };
        };
        std::string errorMessage = "unable to build a type from qualification ";
        errorMessage.append(_qualification->getName());
        DefineAddError(errorMessage)
        DefineReduceAndParse
      };
    DefineParseCase(AfterLogicAndCContextIdentifier)
      { AbstractToken token = arguments.queryToken();
        if (token.getType() == AbstractToken::TOperatorPunctuator) {
          if (((const OperatorPunctuatorToken&) token).getType()
              == OperatorPunctuatorToken::TColonColon) {
            if (_qualification && !_qualification->ssons()) {
              _qualification = NULL;
              DefineGotoCase(AfterQualifiedCContextIdentifier)
            }
            DefineGotoCase(AfterQualifiedLogicAndCContextIdentifier)
          };
        };
        if (_declContext->isRecord()) {
          const clang::RecordDecl* recordDecl =
            static_cast<const clang::RecordDecl*>(_declContext);
          _typeResult =
            arguments.get_clang_utils()->makeLogicType(
              arguments.tokenSourceLocation(),
              recordDecl->getTypeForDecl());
          DefineGotoCaseAndParse(TypeSuffix)
        };
        std::string errorMessage = "unable to build a type from qualification ";
        errorMessage.append(_qualification->getName());
        DefineAddError(errorMessage)
        DefineReduceAndParse
      };
    DefineParseCase(AfterQualifiedLogicIdentifier)
      if (arguments.queryToken().getType() == AbstractToken::TIdentifier) {
        const std::string& identifier = ((const IdentifierToken&)
            arguments.getContentToken()).content();
        assert(_qualification && _qualification->ssons());
        GlobalContext::NestedContext locateSon(identifier);
        const GlobalContext::NestedContext::SonsSet& sons =
          *_qualification->ssons();
        GlobalContext::NestedContext::SonsSet::const_iterator found =
          sons.find(&locateSon);
        if (found != sons.end()) {
          _qualification = *found;
          if (_qualification->ssons())
            DefineGotoCase(AfterLogicIdentifier)
          if (_qualification->isLogicType()) {
            logic_type_info ti = _qualification->asLogicType().type_info();
            _typeResult =
              logic_type_Lnamed(
                qualified_name_dup(ti->type_name),ti->is_extern_c,NULL);
            arguments.extendLocationWithToken(_loc);
            DefineGotoCase(LogicTypeSuffix)
          };
        };
        arguments.extendLocationWithToken(_loc);
        DefineAddError(std::string("identifier '").append(identifier)
            .append("' does not appear to be a type"));
        DefineTReduce
      };
      arguments.extendLocationWithToken(_loc);
      DefineAddError(std::string("expecting idendifier "
            "after parsing a qualification '::'"));
      DefineTReduce
    DefineParseCase(AfterQualifiedLogicAndCContextIdentifier)
      if (arguments.queryToken().getType() == AbstractToken::TIdentifier) {
        const std::string& identifier = ((const IdentifierToken&)
            arguments.getContentToken()).content();
        assert(_qualification && _qualification->ssons() && _declContext);
        GlobalContext::NestedContext locateSon(identifier);
        const GlobalContext::NestedContext::SonsSet& sons =
          *_qualification->ssons();
        GlobalContext::NestedContext::SonsSet::const_iterator found =
          sons.find(&locateSon);
        bool hasFoundLogicQualification = false;
        if (found != sons.end()) {
          _qualification = *found;
          if (_qualification->ssons())
            hasFoundLogicQualification = true;
          if (_qualification->isLogicType()) {
            logic_type_info ti = _qualification->asLogicType().type_info();
            _typeResult =
              logic_type_Lnamed(
                qualified_name_dup(ti->type_name),ti->is_extern_c,NULL);
            arguments.extendLocationWithToken(_loc);
            DefineGotoCase(LogicTypeSuffix)
          };
        };

        const clang::NamedDecl* cidentifier = arguments.findQualifiedName(
            identifier, _declContext);
        if (cidentifier) {
          clang::Decl::Kind kind = cidentifier->getKind();
          if (kind >= clang::Decl::firstRecord
                && kind <= clang::Decl::lastRecord) {
            assert(llvm::dyn_cast<clang::RecordDecl>(cidentifier));
            _declContext = static_cast<const clang::RecordDecl*>(cidentifier);
            arguments.extendLocationWithToken(_loc);
            if (!hasFoundLogicQualification)
              DefineGotoCase(AfterCContextIdentifier)
            else
              DefineGotoCase(AfterLogicAndCContextIdentifier);
          };
          if (kind >= clang::Decl::firstType && kind <= clang::Decl::lastType) {
            if (hasFoundLogicQualification)
              DefineGotoCase(AfterLogicIdentifier);
            _typeResult =
              from_c_named_type(cidentifier,arguments.get_clang_utils());
            arguments.extendLocationWithToken(_loc);
            DefineGotoCase(TypeSuffix)
          };
          
          switch (kind) {
            // case clang::Decl::Label:
            case clang::Decl::Namespace:
              assert(llvm::dyn_cast<clang::NamespaceDecl>(cidentifier));
              _declContext = static_cast<const clang::NamespaceDecl*>(
                  cidentifier);
              if (!hasFoundLogicQualification)
                DefineGotoCase(AfterCContextIdentifier)
              else
                DefineGotoCase(AfterLogicAndCContextIdentifier);
            case clang::Decl::NamespaceAlias:
              assert(llvm::dyn_cast<clang::NamespaceAliasDecl>(cidentifier));
              _declContext = static_cast<const clang::NamespaceAliasDecl*>(
                  cidentifier)->getNamespace();
              if (!hasFoundLogicQualification)
                DefineGotoCase(AfterCContextIdentifier)
              else
                DefineGotoCase(AfterLogicAndCContextIdentifier)
            default:
              break;
          };
        };
        if (hasFoundLogicQualification)
          DefineGotoCase(AfterLogicIdentifier);
        arguments.extendLocationWithToken(_loc);
        DefineAddError(std::string("identifier '").append(identifier)
            .append("' does not appear to be a type"));
        DefineTReduce
      };
      arguments.extendLocationWithToken(_loc);
      DefineAddError(std::string("expecting idendifier "
            "after parsing a qualification '::'"));
      DefineTReduce
    DefineParseCase(AfterCContextIdentifier)
      { AbstractToken token = arguments.queryToken();
        if (token.getType() == AbstractToken::TOperatorPunctuator) {
          if (((const OperatorPunctuatorToken&) token).getType()
              == OperatorPunctuatorToken::TColonColon)
            DefineGotoCase(AfterQualifiedCContextIdentifier)
        };
        if (_declContext->isRecord()) {
          const clang::RecordDecl* recordDecl =
            static_cast<const clang::RecordDecl*>(_declContext);
          _typeResult =
            arguments.get_clang_utils()->makeLogicType(
              arguments.tokenSourceLocation(),
              recordDecl->getTypeForDecl());
          DefineGotoCaseAndParse(TypeSuffix)
        };
        std::string errorMessage = "unable to build a C/C++ type "
          "from qualification ";
        errorMessage.append(_qualification->getName());
        DefineAddError(errorMessage)
        DefineReduceAndParse
      };
    DefineParseCase(AfterQualifiedCContextIdentifier)
      if (arguments.queryToken().getType() == AbstractToken::TIdentifier) {
        const std::string& identifier = ((const IdentifierToken&)
            arguments.getContentToken()).content();
        assert(_declContext);
        const clang::NamedDecl* cidentifier = arguments.findQualifiedName(
            identifier, _declContext);
        if (cidentifier) {
          clang::Decl::Kind kind = cidentifier->getKind();
          if (kind >= clang::Decl::firstRecord
                && kind <= clang::Decl::lastRecord) {
            assert(llvm::dyn_cast<clang::RecordDecl>(cidentifier));
            _declContext = static_cast<const clang::RecordDecl*>(cidentifier);
            arguments.extendLocationWithToken(_loc);
            DefineGotoCase(AfterCContextIdentifier);
          };
          if (kind >= clang::Decl::firstType && kind <= clang::Decl::lastType) {
            _typeResult =
              from_c_named_type(cidentifier,arguments.get_clang_utils());
            arguments.extendLocationWithToken(_loc);
            DefineGotoCase(TypeSuffix)
          };
          
          switch (kind) {
            // case clang::Decl::Label:
            case clang::Decl::Namespace:
              assert(llvm::dyn_cast<clang::NamespaceDecl>(cidentifier));
              _declContext = static_cast<const clang::NamespaceDecl*>(
                  cidentifier);
              DefineGotoCase(AfterCContextIdentifier);
            case clang::Decl::NamespaceAlias:
              assert(llvm::dyn_cast<clang::NamespaceAliasDecl>(cidentifier));
              _declContext = static_cast<const clang::NamespaceAliasDecl*>(
                  cidentifier)->getNamespace();
              DefineGotoCase(AfterCContextIdentifier);
            default:
              break;
          };
        };
        DefineAddError(std::string("unknown identifier '").append(identifier)
            .append("'"));
        DefineReduce
      };
      DefineAddError(std::string("expecting type idendifier "
            "after parsing a qualification '::'"));
      DefineReduce
    DefineParseCase(CTypeSuffix) {// there might be more than one C specifier
        AbstractToken token = arguments.queryToken();
        if (token.getType() == AbstractToken::TKeyword) {
          switch (((const KeywordToken&) token).getType()) {
            case KeywordToken::TChar: {
              // can only be mixed with signed and unsigned
              if (unspecifiedKind()) {
                if (_typeResult->cons_logic_type.Lint.kind == IINT)
                  _typeResult->cons_logic_type.Lint.kind =
                    _seenSigned?ISCHAR:ICHAR;
                else
                  _typeResult->cons_logic_type.Lint.kind = IUCHAR;
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(TypeSuffix) }
              else {
                DefineAddError(
                  "conflicting C type specification in logic type: char");
                DefineReduceAndParse
              }
            }
            case KeywordToken::TConst:
            case KeywordToken::TVolatile:
              // just ignore these arguments, they are irrelevant in the logic
              arguments.extendLocationWithToken(_loc);
              DefineGotoCase(CTypeSuffix)
            case KeywordToken::TInt: {
                // can be mixed with long, short, unsigned, and signed
                if (_typeResult->tag_logic_type == LINT) {
                  if (_seenInt) {
                    DefineAddErrorAndParse(
                      "duplicated 'int' type specification")
                  }
                  switch (_typeResult->cons_logic_type.Lint.kind) {
                    case ISHORT:
                    case IUSHORT:
                    case IINT:
                    case IUINT:
                    case ILONG:
                    case IULONG:
                    case ILONGLONG:
                    case IULONGLONG:
                      break;
                    default:
                      DefineAddErrorAndParse(
                        "unexpected 'int' type specification")
                  }
                  _seenInt = true;
                  arguments.extendLocationWithToken(_loc);
                  DefineGotoCase(CTypeSuffix)
                } else {
                  DefineAddErrorAndParse(
                    "conflicting C type specification in logic type: int")
                }
            }
            case KeywordToken::TUnsigned: {
              if (_seenSigned) {
                DefineAddErrorAndParse(
                  "mixing signed and unsigned type specification")
              } else if (_typeResult->tag_logic_type == LFLOAT) {
                DefineAddErrorAndParse(
                  "'unsigned' meaningless for floating point")
              } else {
                switch (_typeResult->cons_logic_type.Lint.kind) {
                  case IBOOL:
                    DefineAddErrorAndParse("'unsigned' meaningless for boolean")
                  case ICHAR16:
                    DefineAddErrorAndParse("'unsigned' meaningless for char16_t")
                  case ICHAR32:
                    DefineAddErrorAndParse("'unsigned' meaningless for char32_t")
                  case IUCHAR:
                  case IWUCHAR:
                  case IUSHORT:
                  case IUINT:
                  case IULONG:
                  case IULONGLONG:
                    DefineAddErrorAndParse("found 'unsigned' twice")
                  case ICHAR:
                    _typeResult->cons_logic_type.Lint.kind = IUCHAR;
                    break;
                  case IWCHAR:
                    _typeResult->cons_logic_type.Lint.kind = IWUCHAR;
                    break;
                  case ISHORT:
                    _typeResult->cons_logic_type.Lint.kind = IUSHORT;
                    break;
                  case ILONG:
                    _typeResult->cons_logic_type.Lint.kind = IULONG;
                    break;
                  case ILONGLONG:
                    _typeResult->cons_logic_type.Lint.kind = IULONGLONG;
                    break;
                  default:
                    // architecture dependent char types. can't be generated
                    assert(false);
                }
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(CTypeSuffix)
              }
            }
            case KeywordToken::TSigned: {
              if (_seenSigned) {
                DefineAddErrorAndParse("duplicated signed type specification")
              } else if (_typeResult->tag_logic_type == LFLOAT) {
                DefineAddErrorAndParse(
                  "'signed' meaningless for floating point")
              } else {
                switch (_typeResult->cons_logic_type.Lint.kind) {
                  case IBOOL:
                    DefineAddErrorAndParse("'signed' meaningless for boolean")
                  case ICHAR16:
                    DefineAddErrorAndParse("'signed' meaningless for char16_t")
                  case ICHAR32:
                    DefineAddErrorAndParse("'signed' meaningless for char32_t")
                  case IUCHAR:
                  case IWUCHAR:
                  case IUSHORT:
                  case IUINT:
                  case IULONG:
                  case IULONGLONG:
                    DefineAddErrorAndParse(
                      "mixing 'signed' and 'unsigned' in type specification")
                  case ICHAR:
                  case IWCHAR:
                  case ISHORT:
                  case ILONG:
                  case ILONGLONG:
                    break;
                  default: 
                    // architecture dependent char types. can't be generated
                    assert(false);
                }
                _seenSigned = true;
                arguments.extendLocationWithToken(_loc);
              }
              DefineGotoCase(CTypeSuffix)
            }
            case KeywordToken::TLong: {
              if (_typeResult->tag_logic_type == LFLOAT) {
                switch(_typeResult->cons_logic_type.Lfloat.kind) {
                  case FFLOAT:
                    DefineAddErrorAndParse(
                      "unexpected 'long' specification for a float")
                  case FDOUBLE:
                    _typeResult->cons_logic_type.Lfloat.kind = FLONGDOUBLE;
                    DefineGotoCase(TypeSuffix)
                  case FLONGDOUBLE:
                    DefineAddErrorAndParse(
                      "cannot have long long double type in Frama-Clang")
                }
              } else { // integer type
                switch(_typeResult->cons_logic_type.Lint.kind) {
                  case IINT:
                    _typeResult->cons_logic_type.Lint.kind = ILONG;
                    break;
                  case IUINT:
                    _typeResult->cons_logic_type.Lint.kind = IULONG;
                    break;
                  case ILONG:
                    _typeResult->cons_logic_type.Lint.kind = ILONGLONG;
                    break;
                  case IULONG:
                    _typeResult->cons_logic_type.Lint.kind = IULONGLONG;
                    break;
                  case ILONGLONG:
                  case IULONGLONG:
                    DefineAddErrorAndParse(
                      "long long long integer type does not exist")
                  default:
                    DefineAddErrorAndParse(
                      "unexpected 'long' type specification")
                }
                arguments.extendLocationWithToken(_loc);
              }
              DefineGotoCase(CTypeSuffix)
            }
            case KeywordToken::TShort: {
              // can only be mixed with signed, unsigned, and int
              if (unspecifiedKind()) {
                if (_typeResult->cons_logic_type.Lint.kind == IUINT)
                  _typeResult->cons_logic_type.Lint.kind = IUSHORT;
                else
                  _typeResult->cons_logic_type.Lint.kind = ISHORT;
                arguments.extendLocationWithToken(_loc);
                DefineGotoCase(CTypeSuffix)
              }
              else
                DefineAddErrorAndParse(
                  "unexpected 'short' type specification")
            }
            case KeywordToken::TDouble: {
              // only possibility is 'long double'
              if (_typeResult->tag_logic_type == LINT &&
                  _typeResult->cons_logic_type.Lint.kind == ILONG) {
                free_logic_type(_typeResult);
                _typeResult=logic_type_Lfloat(FLONGDOUBLE);
                arguments.extendLocationWithToken(_loc);
                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