fix symbol collision, seen with clang-3.5
autfilt would segfault after reading any file, because the local result_ structure used in hoaparse has the same name as the local result_ structure used in dstarparse. For some reason I can only see this problem using clang-3.5, not with gcc. * src/dstarparse/dstarparse.yy, src/hoaparse/hoaparse.yy: Declare both structures in a different namespace.
This commit is contained in:
Alexandre Duret-Lutz
parent
ee0c0cd28c
commit
d3fdf55fa3
2 changed files with 98 additions and 92 deletions
|
|
@ -1,6 +1,6 @@
|
||||||
/* -*- coding: utf-8 -*-
|
/* -*- coding: utf-8 -*-
|
||||||
** Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
|
** Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
|
||||||
** de l'Epita (LRDE).
|
** Développement de l'Epita (LRDE).
|
||||||
**
|
**
|
||||||
** This file is part of Spot, a model checking library.
|
** This file is part of Spot, a model checking library.
|
||||||
**
|
**
|
||||||
|
|
@ -34,34 +34,37 @@
|
||||||
#include "ltlast/constant.hh"
|
#include "ltlast/constant.hh"
|
||||||
#include "public.hh"
|
#include "public.hh"
|
||||||
|
|
||||||
typedef std::map<int, bdd> map_t;
|
inline namespace dstaryy
|
||||||
|
|
||||||
struct result_
|
|
||||||
{
|
{
|
||||||
spot::dstar_aut_ptr d;
|
typedef std::map<int, bdd> map_t;
|
||||||
spot::ltl::environment* env;
|
|
||||||
std::vector<bdd> guards;
|
|
||||||
std::vector<bdd>::const_iterator cur_guard;
|
|
||||||
map_t dest_map;
|
|
||||||
int cur_state;
|
|
||||||
|
|
||||||
unsigned state_count = 0;
|
struct result_
|
||||||
unsigned start_state = 0;
|
|
||||||
std::vector<std::string> aps;
|
|
||||||
|
|
||||||
bool state_count_seen:1;
|
|
||||||
bool accpair_count_seen:1;
|
|
||||||
bool start_state_seen:1;
|
|
||||||
bool aps_seen:1;
|
|
||||||
|
|
||||||
result_():
|
|
||||||
state_count_seen(false),
|
|
||||||
accpair_count_seen(false),
|
|
||||||
start_state_seen(false),
|
|
||||||
aps_seen(false)
|
|
||||||
{
|
{
|
||||||
}
|
spot::dstar_aut_ptr d;
|
||||||
};
|
spot::ltl::environment* env;
|
||||||
|
std::vector<bdd> guards;
|
||||||
|
std::vector<bdd>::const_iterator cur_guard;
|
||||||
|
map_t dest_map;
|
||||||
|
int cur_state;
|
||||||
|
|
||||||
|
unsigned state_count = 0;
|
||||||
|
unsigned start_state = 0;
|
||||||
|
std::vector<std::string> aps;
|
||||||
|
|
||||||
|
bool state_count_seen:1;
|
||||||
|
bool accpair_count_seen:1;
|
||||||
|
bool start_state_seen:1;
|
||||||
|
bool aps_seen:1;
|
||||||
|
|
||||||
|
result_():
|
||||||
|
state_count_seen(false),
|
||||||
|
accpair_count_seen(false),
|
||||||
|
start_state_seen(false),
|
||||||
|
aps_seen(false)
|
||||||
|
{
|
||||||
|
}
|
||||||
|
};
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
%parse-param {spot::dstar_parse_error_list& error_list}
|
%parse-param {spot::dstar_parse_error_list& error_list}
|
||||||
|
|
|
||||||
|
|
@ -40,76 +40,79 @@
|
||||||
#include "priv/accmap.hh"
|
#include "priv/accmap.hh"
|
||||||
#include "ltlparse/public.hh"
|
#include "ltlparse/public.hh"
|
||||||
|
|
||||||
/* Cache parsed formulae. Labels on arcs are frequently identical
|
inline namespace hoayy
|
||||||
and it would be a waste of time to parse them to formula* over and
|
|
||||||
over, and to register all their atomic_propositions in the
|
|
||||||
bdd_dict. Keep the bdd result around so we can reuse it. */
|
|
||||||
typedef std::map<std::string, bdd> formula_cache;
|
|
||||||
|
|
||||||
typedef std::pair<int, std::string*> pair;
|
|
||||||
typedef typename spot::tgba_digraph::namer<std::string>::type named_tgba_t;
|
|
||||||
|
|
||||||
// Note: because this parser is meant to be used on a stream of
|
|
||||||
// automata, it tries hard to recover from errors, so that we get a
|
|
||||||
// chance to reach the end of the current automaton in order to
|
|
||||||
// process the next one. Several variables below are used to keep
|
|
||||||
// track of various error conditions.
|
|
||||||
enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
|
|
||||||
Implicit_Labels };
|
|
||||||
|
|
||||||
struct result_
|
|
||||||
{
|
{
|
||||||
spot::hoa_aut_ptr h;
|
/* Cache parsed formulae. Labels on arcs are frequently identical
|
||||||
spot::ltl::environment* env;
|
and it would be a waste of time to parse them to formula* over and
|
||||||
formula_cache fcache;
|
over, and to register all their atomic_propositions in the
|
||||||
named_tgba_t* namer = nullptr;
|
bdd_dict. Keep the bdd result around so we can reuse it. */
|
||||||
spot::acc_mapper_int* acc_mapper = nullptr;
|
typedef std::map<std::string, bdd> formula_cache;
|
||||||
std::vector<int> ap;
|
|
||||||
std::vector<bdd> guards;
|
|
||||||
std::vector<bdd>::const_iterator cur_guard;
|
|
||||||
std::vector<bool> declared_states; // States that have been declared.
|
|
||||||
std::vector<std::pair<spot::location, unsigned>> start; // Initial states;
|
|
||||||
std::unordered_map<std::string, bdd> alias;
|
|
||||||
std::unordered_map<std::string, spot::location> props;
|
|
||||||
spot::location states_loc;
|
|
||||||
spot::location ap_loc;
|
|
||||||
spot::location state_label_loc;
|
|
||||||
spot::location accset_loc;
|
|
||||||
spot::acc_cond::mark_t acc_state;
|
|
||||||
spot::acc_cond::mark_t neg_acc_sets = 0U;
|
|
||||||
spot::acc_cond::mark_t pos_acc_sets = 0U;
|
|
||||||
unsigned cur_state;
|
|
||||||
int states = -1;
|
|
||||||
int ap_count = -1;
|
|
||||||
int accset = -1;
|
|
||||||
bdd state_label;
|
|
||||||
bdd cur_label;
|
|
||||||
bool has_state_label = false;
|
|
||||||
bool ignore_more_ap = false; // Set to true after the first "AP:"
|
|
||||||
// line has been read.
|
|
||||||
bool ignore_acc = false; // Set to true in case of missing
|
|
||||||
// Acceptance: lines.
|
|
||||||
bool ignore_acc_silent = false;
|
|
||||||
bool ignore_more_acc = false; // Set to true after the first
|
|
||||||
// "Acceptance:" line has been read.
|
|
||||||
|
|
||||||
label_style_t label_style = Mixed_Labels;
|
typedef std::pair<int, std::string*> pair;
|
||||||
|
typedef typename spot::tgba_digraph::namer<std::string>::type named_tgba_t;
|
||||||
|
|
||||||
bool accept_all_needed = false;
|
// Note: because this parser is meant to be used on a stream of
|
||||||
bool accept_all_seen = false;
|
// automata, it tries hard to recover from errors, so that we get a
|
||||||
bool aliased_states = false;
|
// chance to reach the end of the current automaton in order to
|
||||||
|
// process the next one. Several variables below are used to keep
|
||||||
|
// track of various error conditions.
|
||||||
|
enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
|
||||||
|
Implicit_Labels };
|
||||||
|
|
||||||
bool deterministic = false;
|
struct result_
|
||||||
bool complete = false;
|
|
||||||
|
|
||||||
std::map<std::string, spot::location> labels;
|
|
||||||
|
|
||||||
~result_()
|
|
||||||
{
|
{
|
||||||
delete namer;
|
spot::hoa_aut_ptr h;
|
||||||
delete acc_mapper;
|
spot::ltl::environment* env;
|
||||||
}
|
formula_cache fcache;
|
||||||
};
|
named_tgba_t* namer = nullptr;
|
||||||
|
spot::acc_mapper_int* acc_mapper = nullptr;
|
||||||
|
std::vector<int> ap;
|
||||||
|
std::vector<bdd> guards;
|
||||||
|
std::vector<bdd>::const_iterator cur_guard;
|
||||||
|
std::vector<bool> declared_states; // States that have been declared.
|
||||||
|
std::vector<std::pair<spot::location, unsigned>> start; // Initial states;
|
||||||
|
std::unordered_map<std::string, bdd> alias;
|
||||||
|
std::unordered_map<std::string, spot::location> props;
|
||||||
|
spot::location states_loc;
|
||||||
|
spot::location ap_loc;
|
||||||
|
spot::location state_label_loc;
|
||||||
|
spot::location accset_loc;
|
||||||
|
spot::acc_cond::mark_t acc_state;
|
||||||
|
spot::acc_cond::mark_t neg_acc_sets = 0U;
|
||||||
|
spot::acc_cond::mark_t pos_acc_sets = 0U;
|
||||||
|
unsigned cur_state;
|
||||||
|
int states = -1;
|
||||||
|
int ap_count = -1;
|
||||||
|
int accset = -1;
|
||||||
|
bdd state_label;
|
||||||
|
bdd cur_label;
|
||||||
|
bool has_state_label = false;
|
||||||
|
bool ignore_more_ap = false; // Set to true after the first "AP:"
|
||||||
|
// line has been read.
|
||||||
|
bool ignore_acc = false; // Set to true in case of missing
|
||||||
|
// Acceptance: lines.
|
||||||
|
bool ignore_acc_silent = false;
|
||||||
|
bool ignore_more_acc = false; // Set to true after the first
|
||||||
|
// "Acceptance:" line has been read.
|
||||||
|
|
||||||
|
label_style_t label_style = Mixed_Labels;
|
||||||
|
|
||||||
|
bool accept_all_needed = false;
|
||||||
|
bool accept_all_seen = false;
|
||||||
|
bool aliased_states = false;
|
||||||
|
|
||||||
|
bool deterministic = false;
|
||||||
|
bool complete = false;
|
||||||
|
|
||||||
|
std::map<std::string, spot::location> labels;
|
||||||
|
|
||||||
|
~result_()
|
||||||
|
{
|
||||||
|
delete namer;
|
||||||
|
delete acc_mapper;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
%parse-param {spot::hoa_parse_error_list& error_list}
|
%parse-param {spot::hoa_parse_error_list& error_list}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue