From 0da5f44cd230738fc4e31d7594662f42485c9c9b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 24 Sep 2019 11:48:06 +0200
Subject: [PATCH] fix ARM builds

* spot/misc/bitvect.hh (bitvect_array::at): Fix pointer cast.
* spot/twa/bddprint.cc: Adjust to use signed char* explicitly.
* spot/twaalgos/gtec/gtec.hh: Work around GCC bug #90309.
* .gitlab-ci.yml: Add raspbian build.
---
 .gitlab-ci.yml             | 17 +++++++++++++++++
 spot/misc/bitvect.hh       | 23 ++++++++++++++---------
 spot/twa/bddprint.cc       |  8 ++++----
 spot/twaalgos/gtec/gtec.hh |  6 +++++-
 4 files changed, 40 insertions(+), 14 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 40567ebfa..6db16b71e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -83,6 +83,7 @@ alpine-gcc:
     - ./configure
     - make
     - make check
+    - make distcheck || { chmod -R u+w ./spot-*; false; }
   artifacts:
     when: always
     paths:
@@ -284,3 +285,19 @@ publish-unstable:
     - dput lrde *.changes
     - curl -X POST -F ref=master -F token=$TRIGGER_SPOT_WEB -F "variables[spot_branch]=next" https://gitlab.lrde.epita.fr/api/v4/projects/131/trigger/pipeline
     - curl -X POST -F ref=master -F token=$TRIGGER_SANDBOX https://gitlab.lrde.epita.fr/api/v4/projects/181/trigger/pipeline
+
+raspbian:
+  stage: build
+  tags:
+    - armv7
+  script:
+    - autoreconf -vfi
+    - ./configure
+    - make
+    - make distcheck || { chmod -R u+w ./spot-*; false; }
+  artifacts:
+    when: always
+    paths:
+      - ./spot-*/_build/sub/tests/*/*.log
+      - ./*.log
+      - ./*.tar.gz
diff --git a/spot/misc/bitvect.hh b/spot/misc/bitvect.hh
index cf5771804..330f6045f 100644
--- a/spot/misc/bitvect.hh
+++ b/spot/misc/bitvect.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2013-2019 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -416,13 +416,6 @@ namespace spot
       return size_;
     }
 
-    /// Return the bit-vector at \a index.
-    bitvect& at(const size_t index)
-    {
-      SPOT_ASSERT(index < size_);
-      return *reinterpret_cast<bitvect*>(storage() + index * bvsize_);
-    }
-
     void clear_all()
     {
       // FIXME: This could be changed into a large memset if the
@@ -431,11 +424,23 @@ namespace spot
         at(s).clear_all();
     }
 
+    /// Return the bit-vector at \a index.
+    bitvect& at(const size_t index)
+    {
+      SPOT_ASSERT(index < size_);
+      // The double cast is to prevent -Wcast-align diagnostics
+      // about the fact that char* (the type of storage) has a
+      // smaller required alignment than bitvect*.
+      auto v = static_cast<void*>(storage() + index * bvsize_);
+      return *static_cast<bitvect*>(v);
+    }
+
     /// Return the bit-vector at \a index.
     const bitvect& at(const size_t index) const
     {
       SPOT_ASSERT(index < size_);
-      return *reinterpret_cast<const bitvect*>(storage() + index * bvsize_);
+      auto v = static_cast<const void*>(storage() + index * bvsize_);
+      return *static_cast<const bitvect*>(v);
     }
 
     friend SPOT_API bitvect_array* make_bitvect_array(size_t bitcount,
diff --git a/spot/twa/bddprint.cc b/spot/twa/bddprint.cc
index a0d4b3625..ea0d84c2c 100644
--- a/spot/twa/bddprint.cc
+++ b/spot/twa/bddprint.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2012, 2014, 2015, 2018 Laboratoire de Recherche
-// et Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2012, 2014, 2015, 2018, 2019 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.
@@ -81,7 +81,7 @@ namespace spot
 
   static std::ostream* where;
   static void
-  print_sat_handler(char* varset, int size)
+  print_sat_handler(signed char* varset, int size)
   {
     bool not_first = false;
     for (int v = 0; v < size; ++v)
@@ -111,7 +111,7 @@ namespace spot
 
   static bool first_done = false;
   static void
-  print_accset_handler(char* varset, int size)
+  print_accset_handler(signed char* varset, int size)
   {
     for (int v = 0; v < size; ++v)
       if (varset[v] > 0)
diff --git a/spot/twaalgos/gtec/gtec.hh b/spot/twaalgos/gtec/gtec.hh
index c601ca0d1..c3ddcb0c1 100644
--- a/spot/twaalgos/gtec/gtec.hh
+++ b/spot/twaalgos/gtec/gtec.hh
@@ -125,7 +125,10 @@ namespace spot
   /// \brief An implementation of the Couvreur99 emptiness-check algorithm.
   ///
   /// See the documentation for spot::couvreur99.
-  class SPOT_API couvreur99_check: public emptiness_check, public ec_statistics
+  class SPOT_API couvreur99_check:
+    // We inherit from ec_statistics first to work around GCC bug #90309.
+    // https://gcc.gnu.org/bugzilla/show_bug.cgi?id=90309#c6
+    public ec_statistics, public emptiness_check
   {
   public:
     couvreur99_check(const const_twa_ptr& a, option_map o = option_map());
@@ -160,6 +163,7 @@ namespace spot
     bool poprem_;
     /// Number of dead SCC removed by the algorithm.
     unsigned removed_components;
+
     unsigned get_removed_components() const;
     unsigned get_vmsize() const;
   };