@@ -780,78 +780,133 @@ std::string polyspace::Parser::nextToken()
780780 return token;
781781}
782782
783- void polyspace::Parser::finishSuppression ( )
783+ bool polyspace::Parser::parseAnnotation (polyspace::Annotation &annotation )
784784{
785- Suppression suppr = { mFamily , mResultName , mFilename , 0 , 0 };
785+ annotation.family = nextToken ();
786+ annotation.resultNames .clear ();
787+ annotation.extraComment = " " ;
786788
787- switch (mKind ) {
788- case CommentKind::Regular:
789- {
790- suppr.lineBegin = mLine ;
791- suppr.lineEnd = mLine + mRange ;
792- mDone .push_back (suppr);
793- return ;
794- }
795- case CommentKind::Begin:
796- {
797- suppr.lineBegin = mLine ;
798- mStarted .push_back (suppr);
799- return ;
800- }
801- case CommentKind::End:
802- {
803- auto it = std::find_if (
804- mStarted .begin (),
805- mStarted .end (),
806- [&] (const Suppression &other) {
807- return suppr.matches (other);
808- }
809- );
810-
811- if (it == mStarted .end ())
812- return ;
813-
814- suppr.lineBegin = it->lineBegin ;
815- suppr.lineEnd = mLine ;
816- mStarted .erase (it);
817- mDone .push_back (suppr);
818- return ;
819- }
820- }
821- }
822-
823- bool polyspace::Parser::parseEntry ()
824- {
825- mFamily = nextToken ();
826- if (mFamily .empty ())
789+ if (annotation.family .empty ())
827790 return false ;
828791
829792 if (nextToken () != " :" )
830793 return false ;
831794
832- // Parse result name, multiple names may be separated by commas
833- while (! mComment . empty ()) {
834- mResultName = nextToken ();
835- if (mResultName .empty ())
795+ for (;;) {
796+ const std::string resultName = nextToken ();
797+
798+ if (resultName .empty ())
836799 return false ;
837800
838- finishSuppression ( );
801+ annotation. resultNames . push_back ( std::move (resultName) );
839802
840- if (peekToken () == " ," ) {
803+ if (peekToken (). substr ( 0 , 1 ) == " ," ) {
841804 (void ) nextToken ();
842805 continue ;
843806 }
844807
845808 break ;
846809 }
847810
848- // Skip status and severity
849- if (!peekToken ().empty () && mPeeked [0 ] == ' [' )
811+ if (peekToken ().substr (0 , 1 ) == " [" )
850812 (void ) nextToken ();
851813
814+ if (peekToken ().substr (0 , 1 ) == " \" " ) {
815+ std::string extraComment = nextToken ().substr (1 );
816+
817+ if (extraComment.size () > 1 )
818+ extraComment.pop_back ();
819+
820+ annotation.extraComment = extraComment;
821+ }
822+
852823 return true ;
853824}
854825
826+ polyspace::CommentKind polyspace::Parser::parseKind ()
827+ {
828+ const std::string token = nextToken ();
829+
830+ if (token == " polyspace" )
831+ return CommentKind::Regular;
832+
833+ if (token == " polyspace-begin" )
834+ return CommentKind::Begin;
835+
836+ if (token == " polyspace-end" )
837+ return CommentKind::End;
838+
839+ return CommentKind::Invalid;
840+ }
841+
842+ int polyspace::Parser::parseRange ()
843+ {
844+ if (peekToken ()[0 ] == ' +' ) {
845+ try {
846+ const int range = std::stoi (peekToken ().substr (1 ));
847+ (void ) nextToken ();
848+ return range;
849+ } catch (...) {
850+ return -1 ;
851+ }
852+ }
853+
854+ return 0 ;
855+ }
856+
857+ void polyspace::Parser::handleAnnotation (const polyspace::Annotation &annotation)
858+ {
859+ for (const auto &resultName : annotation.resultNames ) {
860+ Suppression suppr = {
861+ annotation.family ,
862+ resultName,
863+ annotation.filename ,
864+ annotation.extraComment ,
865+ 0 ,
866+ 0 ,
867+ };
868+
869+ switch (annotation.kind ) {
870+ case CommentKind::Regular:
871+ {
872+ suppr.lineBegin = annotation.line ;
873+ suppr.lineEnd = annotation.line + annotation.range ;
874+ mDone .push_back (suppr);
875+ break ;
876+ }
877+ case CommentKind::Begin:
878+ {
879+ suppr.lineBegin = annotation.line ;
880+ mStarted .push_back (suppr);
881+ break ;
882+ }
883+ case CommentKind::End:
884+ {
885+ auto it = std::find_if (
886+ mStarted .begin (),
887+ mStarted .end (),
888+ [&] (const Suppression &other) {
889+ return suppr.matches (other);
890+ }
891+ );
892+
893+ if (it == mStarted .end ())
894+ break ;
895+
896+ suppr.lineBegin = it->lineBegin ;
897+ suppr.lineEnd = annotation.line ;
898+ mStarted .erase (it);
899+ mDone .push_back (suppr);
900+ break ;
901+ }
902+ case CommentKind::Invalid:
903+ {
904+ assert (false ); // Invalid comments are not handled
905+ }
906+ }
907+ }
908+ }
909+
855910void polyspace::Parser::collect (SuppressionList &suppressions) const
856911{
857912 for (const auto &polyspaceSuppr : mDone ) {
@@ -864,6 +919,7 @@ void polyspace::Parser::collect(SuppressionList &suppressions) const
864919 suppr.isInline = true ;
865920 suppr.isPolyspace = true ;
866921 suppr.fileName = polyspaceSuppr.filename ;
922+ suppr.extraComment = polyspaceSuppr.extraComment ;
867923
868924 suppr.lineNumber = polyspaceSuppr.lineBegin ;
869925 if (polyspaceSuppr.lineBegin == polyspaceSuppr.lineEnd ) {
@@ -884,39 +940,28 @@ void polyspace::Parser::parse(const std::string &comment, int line, const std::s
884940 return ;
885941
886942 mComment = comment.substr (2 );
887- mLine = line;
888- mFilename = filename;
889943 mHasPeeked = false ;
890944
891945 while (true ) {
892- const std::string kindStr = nextToken ();
893- if (kindStr. empty () )
946+ const CommentKind kind = parseKind ();
947+ if (kind == CommentKind::Invalid )
894948 return ;
895949
896- if (kindStr == " polyspace" ) mKind = CommentKind::Regular;
897- else if (kindStr == " polyspace-begin" ) mKind = CommentKind::Begin;
898- else if (kindStr == " polyspace-end" ) mKind = CommentKind::End;
899- else return ;
950+ const int range = parseRange ();
951+ if (range < 0 )
952+ return ;
900953
901- mRange = 0 ;
902- if ( peekToken ()[ 0 ] == ' + ' ) {
903- try { mRange = std::stoi ( mPeeked . substr ( 1 )); } catch (...) { return ; }
904- ( void ) nextToken () ;
905- }
954+ Annotation annotation ;
955+ annotation. filename = filename;
956+ annotation. kind = kind;
957+ annotation. line = line ;
958+ annotation. range = range;
906959
907- while (parseEntry ()) {
908- if (peekToken ().empty () || mPeeked [0 ] == ' \" ' )
960+ while (parseAnnotation (annotation)) {
961+ handleAnnotation (annotation);
962+ if (!annotation.extraComment .empty ())
909963 break ;
910964 }
911-
912- if (!peekToken ().empty () && mPeeked [0 ] == ' \" ' ) {
913- (void ) nextToken ();
914- if (peekToken ().empty ())
915- return ;
916- continue ;
917- }
918-
919- break ;
920965 }
921966}
922967
0 commit comments