alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlparse, eltlparse: avoid unnecessary calls to strlen().

Browse source 
* src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh (flex_set_buffer):
Take a std::string as argument and call yy_scan_bytes() with
the string size() instead of calling yy_scan_string() which does
strlen() on the supplied string.
* src/ltlparse/ltlparse.yy: Adjust calls.
* src/eltlparse/eltlscan.ll, src/eltlparse/parsedecl.hh,
src/eltlparse/eltlparse.yy: Use a similar interface.  This
also fixes a memory leak as the scanned buffer was not
released.
This commit is contained in:
Alexandre Duret-Lutz 2014-01-07 16:03:57 +01:00
parent 0c06844655
commit e2143c0313
6 changed files with 36 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/eltlparse/eltlparse.yy
View file

@ -1,6 +1,6 @@
/* -*- coding: utf-8 -*-
** Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de
** Recherche et Développement de l'Epita (LRDE).
** Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire
** de Recherche et Développement de l'Epita (LRDE).
**
** This file is part of Spot, a model checking library.
**
@ -552,7 +552,7 @@ namespace spot
environment& env,
bool debug)
{
flex_scan_string(eltl_string.c_str());
flex_set_buffer(eltl_string);
const formula* result = 0;
nfamap nmap;
aliasmap amap;
@ -561,6 +561,7 @@ namespace spot
parser.set_debug_level(debug);
parser.parse();
error_list = pe.list_;
flex_unset_buffer();
return result;
}
}

18
src/eltlparse/eltlscan.ll
View file

@ -1,4 +1,5 @@
/* Copyright (C) 2008 Laboratoire de Recherche et Développement
/* -*- coding: utf-8 -*-
** Copyright (C) 2008, 2014 Laboratoire de Recherche et Développement
** de l'Epita (LRDE).
**
** This file is part of Spot, a model checking library.
@ -19,6 +20,7 @@
%option noyywrap
%option prefix="eltlyy"
%option outfile="lex.yy.c"
%option stack
%{
#include <string>
@ -190,9 +192,19 @@ namespace spot
}
void
flex_scan_string(const char* s)
flex_set_buffer(const std::string& buf)
{
yy_scan_string(s);
yypush_buffer_state(YY_CURRENT_BUFFER);
(void) yy_scan_bytes(buf.c_str(), buf.size());
yy_push_state(0);
}
void
flex_unset_buffer()
{
(void)&yy_top_state; // shut up a g++ warning.
yy_pop_state();
yypop_buffer_state();
}
}
}

7
src/eltlparse/parsedecl.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2008, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -35,7 +35,8 @@ namespace spot
{
int flex_open(const std::string& name);
void flex_close();
void flex_scan_string(const char* s);
void flex_set_buffer(const std::string& buf);
void flex_unset_buffer();
}
}

12
src/ltlparse/ltlparse.yy
View file

@ -1,6 +1,6 @@
/* -*- coding: utf-8 -*-
** Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
** et Développement de l'Epita (LRDE).
** Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
** Recherche et Développement de l'Epita (LRDE).
** Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
** Université Pierre et Marie Curie.
@ -983,7 +983,7 @@ namespace spot
bool debug, bool lenient)
{
const formula* result = 0;
flex_set_buffer(ltl_string.c_str(),
flex_set_buffer(ltl_string,
ltlyy::parser::token::START_LTL,
lenient);
ltlyy::parser parser(error_list, env, result);
@ -1000,7 +1000,7 @@ namespace spot
bool debug, bool lenient)
{
const formula* result = 0;
flex_set_buffer(ltl_string.c_str(),
flex_set_buffer(ltl_string,
ltlyy::parser::token::START_BOOL,
lenient);
ltlyy::parser parser(error_list, env, result);
@ -1017,7 +1017,7 @@ namespace spot
bool debug)
{
const formula* result = 0;
flex_set_buffer(ltl_string.c_str(),
flex_set_buffer(ltl_string,
ltlyy::parser::token::START_LBT,
false);
ltlyy::parser parser(error_list, env, result);
@ -1035,7 +1035,7 @@ namespace spot
bool lenient)
{
const formula* result = 0;
flex_set_buffer(sere_string.c_str(),
flex_set_buffer(sere_string,
ltlyy::parser::token::START_SERE,
lenient);
ltlyy::parser parser(error_list, env, result);

9
src/ltlparse/ltlscan.ll
View file

@ -1,6 +1,6 @@
/* -*- coding: utf-8 -*-
** Copyright (C) 2010, 2011, 2012, 2013, Laboratoire de Recherche et
** Développement de l'Epita (LRDE).
** Copyright (C) 2010, 2011, 2012, 2013, 2014, Laboratoire de
** Recherche et Développement de l'Epita (LRDE).
** Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
** département Systèmes Répartis Coopératifs (SRC), Université Pierre
** et Marie Curie.
@ -315,10 +315,11 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
%%
void
flex_set_buffer(const char* buf, int start_tok, bool lenient)
flex_set_buffer(const std::string& buf,
int start_tok, bool lenient)
{
yypush_buffer_state(YY_CURRENT_BUFFER);
yy_scan_string(buf);
(void) yy_scan_bytes(buf.c_str(), buf.size());
start_token = start_tok;
if (start_tok == token::START_LBT)
yy_push_state(lbt);

4
src/ltlparse/parsedecl.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche et
// Copyright (C) 2010, 2012, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE)
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -32,7 +32,7 @@
spot::ltl::parse_error_list& error_list)
YY_DECL;
void flex_set_buffer(const char *buf, int start_tok, bool lenient);
void flex_set_buffer(const std::string& buf, int start_tok, bool lenient);
void flex_unset_buffer();
#endif // SPOT_LTLPARSE_PARSEDECL_HH