From 2f3bbfc45e4fd55afdd4e3f4dab074149c026ecd Mon Sep 17 00:00:00 2001
From: Franck Vedrine <franck.vedrine@cea.fr>
Date: Tue, 3 Nov 2020 16:23:17 +0100
Subject: [PATCH] remove some fall-through warnings

---
 ACSLComment.cpp          |  6 +++---
 ACSLComment.h            |  4 ++--
 ACSLGlobalAnnotation.cpp |  4 ++++
 ACSLLexer.cpp            | 24 ++++++++++++++++++++----
 ACSLLexer.h              |  1 -
 ACSLTermOrPredicate.cpp  |  3 +++
 AnnotationComment.h      |  2 +-
 ClangVisitor.cpp         | 15 ++++++++++++++-
 Clang_utils.cpp          |  2 ++
 Clang_utils.h            |  2 ++
 FramaCIRGen.cpp          |  7 +++----
 11 files changed, 54 insertions(+), 16 deletions(-)

diff --git a/ACSLComment.cpp b/ACSLComment.cpp
index 8e7a617..6943863 100644
--- a/ACSLComment.cpp
+++ b/ACSLComment.cpp
@@ -35,7 +35,7 @@
 #include <string>
 
 bool
-ACSLComment::checkAnnotation(const std::string& text, clang::SourceLocation clangLocation, const clang::Sema* sema, std::string& revised) {
+ACSLComment::checkAnnotation(const std::string& text, clang::SourceLocation clangLocation, const clang::Sema* sema, std::string& revised) const {
 
   Acsl::Lexer lexer(sema);
   // We check the preprocessing directives by using builtin lexing (that is, not clang),
@@ -65,7 +65,7 @@ ACSLComment::checkAnnotation(const std::string& text, clang::SourceLocation clan
 }
 
 ACSLComment::Kind
-ACSLComment::getAnnotationKind(const std::string& text, clang::SourceLocation clangLocation, const clang::Sema* sema) {
+ACSLComment::getAnnotationKind(const std::string& text, clang::SourceLocation clangLocation, const clang::Sema* sema) const {
 
   const char* start = text.c_str();
   size_t length = text.size();
@@ -88,7 +88,7 @@ ACSLComment::getAnnotationKind(const std::string& text, clang::SourceLocation cl
     return KUndefined;
   }
 
-  Acsl::DLexer::KeywordToken key = (Acsl::DLexer::KeywordToken&)t;
+  Acsl::DLexer::KeywordToken key = (const Acsl::DLexer::KeywordToken&)t;
   Acsl::DLexer::KeywordToken::Type ktype = (Acsl::DLexer::KeywordToken::Type)key.getType();
 
   std::string firstWord;
diff --git a/ACSLComment.h b/ACSLComment.h
index 9cf47b9..31ba59f 100644
--- a/ACSLComment.h
+++ b/ACSLComment.h
@@ -58,9 +58,9 @@ public:
     : AnnotationComment(source), _startOfGhost(source._startOfGhost) {}
 
   /*! checks annotation for improper use of preprocessor directives, returns true if errors found */
-  virtual bool checkAnnotation(const std::string& text, clang::SourceLocation clangLocation, const clang::Sema* sema, std::string& revised) ;
+  virtual bool checkAnnotation(const std::string& text, clang::SourceLocation clangLocation, const clang::Sema* sema, std::string& revised) const;
 
-  virtual Kind getAnnotationKind(const std::string& text, clang::SourceLocation clangLocation, const clang::Sema* sema) ;
+  virtual Kind getAnnotationKind(const std::string& text, clang::SourceLocation clangLocation, const clang::Sema* sema) const;
 
   virtual void parseGlobal(ForwardReferenceList& globals,
     ForwardReferenceList* classContent, const clang::DeclContext* clangContext,
diff --git a/ACSLGlobalAnnotation.cpp b/ACSLGlobalAnnotation.cpp
index 42e4c3f..46abe2a 100644
--- a/ACSLGlobalAnnotation.cpp
+++ b/ACSLGlobalAnnotation.cpp
@@ -804,6 +804,8 @@ LAfterQualification:
           };
         };
       };
+      DefineAddError("expecting a '{' after 'axiomatic id '")
+      DefineGotoCaseAndParse(BeforeSemiColon)
    DefineParseCase(AfterAxiomaticBody)
      { AbstractToken token = arguments.queryToken();
        if (token.getType() == AbstractToken::TOperatorPunctuator) {
@@ -968,6 +970,7 @@ LAfterQualification:
           }
         };
         DefineAddError("expecting assignment '=' after 'logic type-var'")
+        DefineGotoCaseAndParse(BeforeSemiColon)
       };
     DefineParseCase(TypeDef)
       { Parser::State::RuleAccess::TCastFromRule<LogicType>
@@ -1149,6 +1152,7 @@ LAfterQualification:
       DefineGotoCase(EndTypeInvariant)
     DefineParseCase(Inductive)
       DefineAddError("unimplemented case")
+      DefineGotoCaseAndParse(BeforeSemiColon)
 
     DefineParseCase(Global)
       { AbstractToken token = arguments.queryToken();
diff --git a/ACSLLexer.cpp b/ACSLLexer.cpp
index eaea59c..caf93f6 100644
--- a/ACSLLexer.cpp
+++ b/ACSLLexer.cpp
@@ -805,7 +805,7 @@ const std::string Lexer::getPreprocessorToken(const std::string& buffer, size_t&
   while (isalnum(ch) || ch == '_' ) { // FIXME - also $?
     ch = advanceChar1NoToken(buffer,position,loc);
   }
-  if (p != position) {
+  if ((size_t) p != position) {
     // An identifiers preprocessor token
     const std::string id = std::string(buffer,p,position-p);
     if (!raw) {
@@ -830,7 +830,7 @@ const std::string Lexer::getPreprocessorToken(const std::string& buffer, size_t&
   while (!isalnum(ch) && ch != '_' && !isspace(ch) && ch != '@' && ch != '\0') {
     ch = advanceChar1NoToken(buffer,position,loc);
   }
-  if (position != p) advanceChar1NoToken(buffer,position,loc);
+  if (position != (size_t) p) advanceChar1NoToken(buffer,position,loc);
   return std::string(buffer,p,position-p);
   // FIXME - what about non-printable tokens or illegal tokens
 }
@@ -1998,12 +1998,12 @@ const std::string Lexer::skipToNextPPDirective(const std::string& buffer, size_t
     skipSpace(buffer, position, loc); // Use this routine so lines are properly counted
     ch = buffer[position];
     if (ch == '\0') return ""; // No token found
-    bool atLineStart = n != loc->linenum1;
+    bool atLineStart = (size_t) n != loc->linenum1;
     if (atLineStart && ch == '#') {
       n = loc->linenum1;
       advanceChar1NoToken(buffer,position,loc);
       skipSpace(buffer,position,loc);
-      if (n != loc->linenum1) {
+      if ((size_t) n != loc->linenum1) {
         // FIXME - does not handle lines with only comments after the #
         // Empty directive
         return std::string(" ");
@@ -2311,6 +2311,7 @@ Lexer::convertClangTokenToACSLToken(const clang::Token& source) const {
     case clang::tok::hashhash:
     case clang::tok::hashat:
       notImplemented(source);
+      assert(false);
 
     // C++ Support
     case clang::tok::periodstar:
@@ -2331,6 +2332,7 @@ Lexer::convertClangTokenToACSLToken(const clang::Token& source) const {
     case clang::tok::lesslessless:
     case clang::tok::greatergreatergreater:
       notImplemented(source);
+      assert(false);
 
     // C99 6.4.1: Keywords.  These turn into kw_* tokens.
     case clang::tok::kw_auto:
@@ -2338,6 +2340,7 @@ Lexer::convertClangTokenToACSLToken(const clang::Token& source) const {
           .setType(DLexer::KeywordToken::TAuto));
     case clang::tok::kw_break:
       notImplemented(source);
+      assert(false);
       // return DLexer::Token(DLexer::KeywordToken()
       //     .setType(DLexer::KeywordToken::TBreak));
     case clang::tok::kw_case:
@@ -2351,6 +2354,7 @@ Lexer::convertClangTokenToACSLToken(const clang::Token& source) const {
           .setType(DLexer::KeywordToken::TConst));
     case clang::tok::kw_continue:
       notImplemented(source);
+      assert(false);
       // return DLexer::Token(DLexer::KeywordToken()
       //     .setType(DLexer::KeywordToken::TContinue));
     case clang::tok::kw_default:
@@ -2496,18 +2500,22 @@ Lexer::convertClangTokenToACSLToken(const clang::Token& source) const {
           .setType(DLexer::KeywordToken::TFalse));
     case clang::tok::kw_friend:
       notImplemented(source);
+      assert(false);
       // return DLexer::Token(DLexer::KeywordToken()
       //     .setType(DLexer::KeywordToken::TFriend));
     case clang::tok::kw_mutable:
       notImplemented(source);
+      assert(false);
       // return DLexer::Token(DLexer::KeywordToken()
       //     .setType(DLexer::KeywordToken::TMutable));
     case clang::tok::kw_namespace:
       notImplemented(source);
+      assert(false);
       // return DLexer::Token(DLexer::KeywordToken()
       //     .setType(DLexer::KeywordToken::TNamespace));
     case clang::tok::kw_new:
       notImplemented(source);
+      assert(false);
       // return DLexer::Token(DLexer::KeywordToken()
       //     .setType(DLexer::KeywordToken::TNew));
     case clang::tok::kw_operator:
@@ -2515,14 +2523,17 @@ Lexer::convertClangTokenToACSLToken(const clang::Token& source) const {
           .setType(DLexer::KeywordToken::TOperator));
     case clang::tok::kw_private:
       notImplemented(source);
+      assert(false);
       // return DLexer::Token(DLexer::KeywordToken()
       //     .setType(DLexer::KeywordToken::TPrivate));
     case clang::tok::kw_protected:
       notImplemented(source);
+      assert(false);
       // return DLexer::Token(DLexer::KeywordToken()
       //     .setType(DLexer::KeywordToken::TProtected));
     case clang::tok::kw_public:
       notImplemented(source);
+      assert(false);
       // return DLexer::Token(DLexer::KeywordToken()
       //     .setType(DLexer::KeywordToken::TPublic));
     case clang::tok::kw_reinterpret_cast:
@@ -2533,6 +2544,7 @@ Lexer::convertClangTokenToACSLToken(const clang::Token& source) const {
           .setType(DLexer::KeywordToken::TStaticCast));
     case clang::tok::kw_template:
       notImplemented(source);
+      assert(false);
       // return DLexer::Token(DLexer::KeywordToken()
       //     .setType(DLexer::KeywordToken::TTemplate));
     case clang::tok::kw_this:
@@ -2542,6 +2554,7 @@ Lexer::convertClangTokenToACSLToken(const clang::Token& source) const {
       }
     case clang::tok::kw_throw:
       notImplemented(source);
+      assert(false);
       // return DLexer::Token(DLexer::KeywordToken()
       //     .setType(DLexer::KeywordToken::TThrow));
     case clang::tok::kw_true:
@@ -2549,6 +2562,7 @@ Lexer::convertClangTokenToACSLToken(const clang::Token& source) const {
           .setType(DLexer::KeywordToken::TTrue));
     case clang::tok::kw_try:
       notImplemented(source);
+      assert(false);
       // return DLexer::Token(DLexer::KeywordToken()
       //     .setType(DLexer::KeywordToken::TTry));
     case clang::tok::kw_typename:
@@ -2556,10 +2570,12 @@ Lexer::convertClangTokenToACSLToken(const clang::Token& source) const {
           .setType(DLexer::KeywordToken::TTypename));
     case clang::tok::kw_typeid:
       notImplemented(source);
+      assert(false);
       // return DLexer::Token(DLexer::KeywordToken()
       //     .setType(DLexer::KeywordToken::TTypeid));
     case clang::tok::kw_using:
       notImplemented(source);
+      assert(false);
       // return DLexer::Token(DLexer::KeywordToken()
       //     .setType(DLexer::KeywordToken::TUsing));
     case clang::tok::kw_virtual:
diff --git a/ACSLLexer.h b/ACSLLexer.h
index 301fe47..41b5966 100644
--- a/ACSLLexer.h
+++ b/ACSLLexer.h
@@ -380,7 +380,6 @@ protected:
    void lexUsingClang(const clang::Sema* _sema, const std::string& input, clang::SourceLocation loc, std::list<clang::Token>& clangTokens);
 
 private:
-
    Lexer(const Lexer& source) = delete;
 
 public:
diff --git a/ACSLTermOrPredicate.cpp b/ACSLTermOrPredicate.cpp
index a3b9659..2f90271 100644
--- a/ACSLTermOrPredicate.cpp
+++ b/ACSLTermOrPredicate.cpp
@@ -8222,6 +8222,7 @@ TermOrPredicate::readToken(Parser::State& state, Parser::Arguments& arguments) {
           DefineShift(EndSizeOf, *subTerm, &TermOrPredicate::readToken);
         }
       };
+      DefineGotoCase(EndSizeOf)
     DefineParseCase(EndSizeOf)
       assert(_startLocation);
       { AbstractToken token = arguments.queryToken();
@@ -9260,6 +9261,7 @@ TermOrPredicate::Binders::readToken(Parser::State& state,
         _currentDeclType = rule->extractType();
         state.freeRuleResult();
       };
+      DefineReduceAndParse
     // We'll recurse to check for multiple '*', but we only have to extract
     // the specifier once. AfterType thus falls through 
     // the main part of the rule which starts here.
@@ -9804,6 +9806,7 @@ TermOrPredicate::WithConstruct::readToken(Parser::State& state,
         _node = term_cons(term_node_TUpdate(_node, offset, updateNode),
             loc, NULL);
       };
+      DefineGotoCase(End)
     DefineParseCase(End)
       { AbstractToken token = arguments.queryToken();
         if (token.getType() == AbstractToken::TOperatorPunctuator) {
diff --git a/AnnotationComment.h b/AnnotationComment.h
index 9258e97..b81b4e7 100644
--- a/AnnotationComment.h
+++ b/AnnotationComment.h
@@ -149,7 +149,7 @@ public:
   virtual void parseStatementAnnotation(ForwardReferenceList& codeContainer,
     const clang::DeclContext* clangContext, clang::ASTContext* astContext,
     clang::Sema* sema, clang::Scope* scope, Clang_utils* clangUtils,
-    const RTTITable& rttiTable, location loc) {assert(0);}
+    const RTTITable& rttiTable) {assert(0);}
   virtual void parseFunctionContract(option& /* function_contract */ contract,
     const clang::DeclContext* clangContext, clang::ASTContext* astContext,
     clang::Sema* sema, clang::Scope* scope, Clang_utils* clangUtils,
diff --git a/ClangVisitor.cpp b/ClangVisitor.cpp
index 39eb1b4..53e0bd0 100644
--- a/ClangVisitor.cpp
+++ b/ClangVisitor.cpp
@@ -2874,6 +2874,13 @@ exp_node FramacVisitor::makeExpression(
           expr->dump(llvm::errs(), _context->getSourceManager());
           std::cerr << "\nAborting\n";
           exit(2);
+          // default:
+          //   std::cerr << "Unsupported binary expression:";
+          //   expr->dump(llvm::errs(), _context->getSourceManager());
+          //   std::cerr << "\nAborting\n";
+          //   exit(2);
+          default:
+            break;
         };
         exp_node lhsPart = makeExpression(binaryOperator->getLHS(),
                                           shouldDelay,receiver);
@@ -3323,6 +3330,7 @@ exp_node FramacVisitor::makeExpression(
               _clangUtils->makeType(expr->getExprLoc(), type)),
             expr);
         }
+        assert(false);
       };
     case clang::Stmt::CXXDefaultInitExprClass:
       { assert (llvm::dyn_cast<clang::CXXDefaultInitExpr>(expr));
@@ -3402,6 +3410,7 @@ exp_node FramacVisitor::makeExpression(
             std::cerr <<
             "Unsupported type (record) for default init with braces"
             << std::endl;
+            return NULL;
           default:
             return  guard.setAssignResult(
                       makeExpression(
@@ -3518,6 +3527,8 @@ compilation_constant FramacVisitor::makeConstantExpression(
           std::cerr << "\nAborting\n";
           exit(2);
         }
+      default:
+        break;
     }
   };
   std::cerr << "constant expression cannot be evaluated at compile-time";
@@ -5538,7 +5549,7 @@ LAddSema:
   };
 
   comment.parseStatementAnnotation(*container, clangContext, _context, _sema,
-      scope, _clangUtils, _rttiTable, loc);
+      scope, _clangUtils, _rttiTable);
 
   if (foundBlock) {
     _sema->PopCompoundScope();
@@ -5955,6 +5966,7 @@ void FramacVisitor::readRecordComments(
           //     .getContent());
           break;
         };
+        break;
       default:
         parseDefaultComment(*_annotationCommentList[previousTemplateComment]);
         break;
@@ -5984,6 +5996,7 @@ void FramacVisitor::readRecordComments(
           //     .getContent());
           break;
         };
+        break;
       default:
         parseDefaultComment(*_annotationCommentList[previousComment]);
         break;
diff --git a/Clang_utils.cpp b/Clang_utils.cpp
index d48e932..b5318fb 100644
--- a/Clang_utils.cpp
+++ b/Clang_utils.cpp
@@ -182,6 +182,8 @@ compare_typ(typ t1, typ t2) {
           }
         }
         break;
+      default:
+        break;
     }
   };
   return result;
diff --git a/Clang_utils.h b/Clang_utils.h
index e08eea7..0d0c568 100644
--- a/Clang_utils.h
+++ b/Clang_utils.h
@@ -49,6 +49,8 @@
 #ifdef __GNUC__
 #pragma GCC diagnostic pop
 #endif
+#include "clang/Basic/SourceManager.h"
+#include "clang/Basic/FileManager.h"
 
 extern "C" {
 #include "intermediate_format.h"
diff --git a/FramaCIRGen.cpp b/FramaCIRGen.cpp
index 102f5b7..62be693 100644
--- a/FramaCIRGen.cpp
+++ b/FramaCIRGen.cpp
@@ -192,19 +192,18 @@ ProcessArguments::process(char** argument, int& currentArgument) {
         else {
           currentArgument--;
           _doesGenerateBareFunctions=true;
-          return true;
         }
+        return true;
       case '-':
         if (strcmp(argument[0],"--stop-annot-error")==0) {
           _doesStopAnnotError=true;
           --currentArgument;
-          return true;
         }
-        if (strcmp(argument[0],"--gen-impl-meth")==0) {
+        else if (strcmp(argument[0],"--gen-impl-meth")==0) {
           _doesGenerateImplicitMethods=true;
           --currentArgument;
-          return true;
         }
+        return true;
       default:
         --currentArgument;
         return true;
-- 
GitLab