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

mealy: work around spurious nullptr warning

Browse source 
* spot/twaalgos/mealy_machine.cc (mm_sat_prob_t<true>::get_sol): Call
SPOT_ASSUME to hint that res.data() is not null.
This commit is contained in:
Alexandre Duret-Lutz 2021-08-02 09:28:14 +02:00
parent 3614cf34a8
commit c58e6f22ac
1 changed files with 7 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

13
spot/twaalgos/mealy_machine.cc
View file

@ -2071,25 +2071,26 @@ namespace
get_sol() get_sol()
{ {
// Returns a vector of assignments // Returns a vector of assignments
// The vector is empty iff the the prob is unsat // The vector is empty iff the prob is unsat
// res[i] == -1 : i not used in lit mapper // res[i] == -1 : i not used in lit mapper
// res[i] == 0 : i is assigned false // res[i] == 0 : i is assigned false
// res[i] == 1 : i is assigned true // res[i] == 1 : i is assigned true
switch (picosat_sat(lm.psat_, -1)) switch (picosat_sat(lm.psat_, -1))
{ {
case(PICOSAT_UNSATISFIABLE): case PICOSAT_UNSATISFIABLE:
return {}; return {};
case(PICOSAT_SATISFIABLE): case PICOSAT_SATISFIABLE:
{ {
std::vector<int> std::vector<int>
res(1 + (unsigned) picosat_variables(lm.psat_), -1); res(1 + (unsigned) picosat_variables(lm.psat_), -1);
SPOT_ASSUME(res.data()); // g++ 11 believes data might be nullptr
res[0] = 0; // Convention res[0] = 0; // Convention
for (int lit : lm.all_lits) for (int lit : lm.all_lits)
res.at(lit) = picosat_deref(lm.psat_, lit); res[lit] = picosat_deref(lm.psat_, lit);
#ifdef TRACE #ifdef TRACE
trace << "Sol is \n"; trace << "Sol is\n";
for (unsigned i = 0; i < res.size(); ++i) for (unsigned i = 0; i < res.size(); ++i)
std::cerr << i << " : " << res.at(i) << '\n'; trace << i << ": " << res[i] << '\n';
#endif #endif
return res; return res;
} }