ACSLGlobalAnnotation.h

/**************************************************************************/
/*                                                                        */
/*  This file is part of Frama-Clang                                      */
/*                                                                        */
/*  Copyright (C) 2012-2021                                               */
/*    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:
//   Definition of the ACSL global annotations.
//

#ifndef ACSL_GlobalAnnotationH
#define ACSL_GlobalAnnotationH

#include "ACSLParser.h"
// #include "DescentParse.h"

extern "C" {
#include "intermediate_format.h"
} // end of extern "C"

#include "ACSLLogicType.h"
#include "ACSLTermOrPredicate.h"

namespace Acsl {

/*! @class GlobalAnnotation
 *  @brief Component that parses a global annotation with a state machine.
 *
 *  The state is defined by the Parser::State::point() method and has
 *    additional information within the fields typeVar, _term, _pred,
 *    _params, _typeVarBinders, _polyId, _polyIdLabels, _typeName
 */
class GlobalAnnotation : public ::Parser::Base::RuleResult,
    public ::Parser::Base {
private:
  list _annots;
  ForwardReferenceList _globals;
  location _loc;
  logic_type _typeVar;
  term _term;
  predicate_named _pred;
  bool _hasReads;
  bool _isMethod;
  ForwardList _reads;
  /* logic_arg_decl */ list _params;
  std::list<std::string> _typeVarBinders;
  GlobalContext::Qualification* _qualificationId;
  std::string _polyId;
  std::string _polyAxiomId;
  /* logic_label */ list _polyIdLabels;
  DLexer::OperatorPunctuatorToken::Type _codeOperator;
  qualified_name _typeName;