@@ -780,78 +780,134 @@ 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.substr (0 , extraComment.size () - 1 );
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+ int range;
846+ try {
847+ range = std::stoi (peekToken ().substr (1 ));
848+ } catch (...) {
849+ return -1 ;
850+ }
851+ (void ) nextToken ();
852+ return range;
853+ }
854+
855+ return 0 ;
856+ }
857+
858+ void polyspace::Parser::handleAnnotation (const polyspace::Annotation &annotation)
859+ {
860+ for (const auto &resultName : annotation.resultNames ) {
861+ Suppression suppr = {
862+ annotation.family ,
863+ resultName,
864+ annotation.filename ,
865+ annotation.extraComment ,
866+ 0 ,
867+ 0 ,
868+ };
869+
870+ switch (annotation.kind ) {
871+ case CommentKind::Regular:
872+ {
873+ suppr.lineBegin = annotation.line ;
874+ suppr.lineEnd = annotation.line + annotation.range ;
875+ mDone .push_back (suppr);
876+ break ;
877+ }
878+ case CommentKind::Begin:
879+ {
880+ suppr.lineBegin = annotation.line ;
881+ mStarted .push_back (suppr);
882+ break ;
883+ }
884+ case CommentKind::End:
885+ {
886+ auto it = std::find_if (
887+ mStarted .begin (),
888+ mStarted .end (),
889+ [&] (const Suppression &other) {
890+ return suppr.matches (other);
891+ }
892+ );
893+
894+ if (it == mStarted .end ())
895+ break ;
896+
897+ suppr.lineBegin = it->lineBegin ;
898+ suppr.lineEnd = annotation.line ;
899+ mStarted .erase (it);
900+ mDone .push_back (suppr);
901+ break ;
902+ }
903+ case CommentKind::Invalid:
904+ {
905+ assert (false ); // Invalid comments are not handled
906+ }
907+ }
908+ }
909+ }
910+
855911void polyspace::Parser::collect (SuppressionList &suppressions) const
856912{
857913 for (const auto &polyspaceSuppr : mDone ) {
@@ -864,6 +920,7 @@ void polyspace::Parser::collect(SuppressionList &suppressions) const
864920 suppr.isInline = true ;
865921 suppr.isPolyspace = true ;
866922 suppr.fileName = polyspaceSuppr.filename ;
923+ suppr.extraComment = polyspaceSuppr.extraComment ;
867924
868925 suppr.lineNumber = polyspaceSuppr.lineBegin ;
869926 if (polyspaceSuppr.lineBegin == polyspaceSuppr.lineEnd ) {
@@ -884,39 +941,28 @@ void polyspace::Parser::parse(const std::string &comment, int line, const std::s
884941 return ;
885942
886943 mComment = comment.substr (2 );
887- mLine = line;
888- mFilename = filename;
889944 mHasPeeked = false ;
890945
891946 while (true ) {
892- const std::string kindStr = nextToken ();
893- if (kindStr. empty () )
947+ const CommentKind kind = parseKind ();
948+ if (kind == CommentKind::Invalid )
894949 return ;
895950
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 ;
951+ const int range = parseRange ();
952+ if (range < 0 )
953+ return ;
900954
901- mRange = 0 ;
902- if ( peekToken ()[ 0 ] == ' + ' ) {
903- try { mRange = std::stoi ( mPeeked . substr ( 1 )); } catch (...) { return ; }
904- ( void ) nextToken () ;
905- }
955+ Annotation annotation ;
956+ annotation. filename = filename;
957+ annotation. kind = kind;
958+ annotation. line = line ;
959+ annotation. range = range;
906960
907- while (parseEntry ()) {
908- if (peekToken ().empty () || mPeeked [0 ] == ' \" ' )
961+ while (parseAnnotation (annotation)) {
962+ handleAnnotation (annotation);
963+ if (!annotation.extraComment .empty ())
909964 break ;
910965 }
911-
912- if (!peekToken ().empty () && mPeeked [0 ] == ' \" ' ) {
913- (void ) nextToken ();
914- if (peekToken ().empty ())
915- return ;
916- continue ;
917- }
918-
919- break ;
920966 }
921967}
922968
0 commit comments