From 803a61a03d861ae56fec58938756278bd32da0a6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 16 Apr 2021 18:04:41 +0200 Subject: [PATCH] parse_aut: add support for #line Fixes issue #232. * spot/parseaut/parseaut.yy, spot/parseaut/public.hh, spot/parseaut/scanaut.ll: Add support for #line. * tests/core/parseaut.test: Test it. * NEWS: Mention it. --- NEWS | 6 ++++++ spot/parseaut/parseaut.yy | 6 ++++++ spot/parseaut/public.hh | 2 +- spot/parseaut/scanaut.ll | 23 ++++++++++++++++++++- tests/core/parseaut.test | 42 ++++++++++++++++++++++++++------------- 5 files changed, 63 insertions(+), 16 deletions(-) diff --git a/NEWS b/NEWS index 3f0384069..35b7ca790 100644 --- a/NEWS +++ b/NEWS @@ -191,6 +191,12 @@ New in spot 2.9.6.dev (not yet released) setting SPOT_SIMULATION_REDUCTION environment variable or using the "-x simul-method=..." option (see spot-x(7)). + - The automaton parser will now recognize lines of the form + #line 10 "filename" + that may occur *between* the automata of an input stream to specify + that error messages should be emitted as if the next automaton + was read from "filename" starting on line 10. (Issue #232) + Python: - Bindings for functions related to games. diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index f42f92876..2346bd242 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -255,6 +255,7 @@ extern "C" int strverscmp(const char *s1, const char *s2); %token ACCPAIRS "Acceptance-Pairs:" %token ACCSIG "Acc-Sig:"; %token ENDOFHEADER "---"; +%token LINEDIRECTIVE "#line" %left '|' @@ -338,6 +339,10 @@ extern "C" int strverscmp(const char *s1, const char *s2); %% aut: aut-1 { res.h->loc = @$; YYACCEPT; } +/* Not how we do not accept garbage before LINEDIRECTIVE. This is because + all error will be relative to the specified filename, so that filename + must not be changed after any error was reported. */ + | LINEDIRECTIVE { res.h->filename = *$1; } aut | ENDOFFILE { YYABORT; } | error ENDOFFILE { YYABORT; } | error aut-1 @@ -2635,6 +2640,7 @@ namespace spot check_version(r); last_loc = r.h->loc; last_loc.step(); + filename_ = r.h->filename; // in case it was changed if (r.h->aborted) { if (opts_.ignore_abort) diff --git a/spot/parseaut/public.hh b/spot/parseaut/public.hh index b6332dd36..342057407 100644 --- a/spot/parseaut/public.hh +++ b/spot/parseaut/public.hh @@ -69,7 +69,7 @@ namespace spot /// Format of the automaton. parsed_aut_type type = parsed_aut_type::Unknown; /// Name of the stream (used for displaying syntax errors) - const std::string filename; + std::string filename; /// \brief Syntax errors that occurred during parsing. /// /// Note that the parser does not print any diagnostic. diff --git a/spot/parseaut/scanaut.ll b/spot/parseaut/scanaut.ll index cb54a0af7..fdb6deb9b 100644 --- a/spot/parseaut/scanaut.ll +++ b/spot/parseaut/scanaut.ll @@ -1,5 +1,5 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2014-2018, 2020 Laboratoire de Recherche et Développement +** Copyright (C) 2014-2018, 2020, 2021 Laboratoire de Recherche et Développement ** de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. @@ -90,6 +90,27 @@ identifier [[:alpha:]_][[:alnum:]_.-]* BEGIN(in_COMMENT); yyextra->comment_level = 1; } +"#line"[ \t]+[0-9]+[ \t]+\"[^\"\n]*\" { + errno = 0; + char* end; + unsigned long n = strtoul(yytext + 5, &end, 10); + yylval->num = n; + if (errno || yylval->num != n) + { + error_list.push_back(spot::parse_aut_error(*yylloc, "value too large")); } + else if (error_list.empty()) + { + char* beg = strchr(end, '"'); + end = strrchr(beg + 1, '"'); + yylval->str = new std::string(beg + 1, end); + yylloc->initialize(nullptr, n - 1, yylloc->begin.column); + return token::LINEDIRECTIVE; + } + else + { + error_list.push_back(spot::parse_aut_error(*yylloc, "#line may not occur after any error")); + } + } "HOA:" BEGIN(in_HOA); return token::HOA; "--ABORT--" BEGIN(INITIAL); throw spot::hoa_abort{*yylloc}; "never" BEGIN(in_NEVER); return token::NEVER; diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test index a4f273608..c882b4093 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014-2018, 2020 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2014-2018, 2020-2021 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -69,6 +69,7 @@ input:2.1-9: ... previously defined here. EOF cat >input <input <input <input <