Github: related to #189 "TSX"

Github: related to #189 "TSX"

This option is not yet used for anything.

Github: related to #189 "TSX"

Github: related to #189 "TSX"

It's unclear what the breaking change is in Python 3.8 now, but the macOS builds
were still failing, this time claiming that config was None. This time we try to
work around it by not relying on any complex globals and instead storing the
(duplicate) config within the test cases themselves.

It turns out you are not meant to share memory between Python multiprocesses
unless you explicitly declare it. I think we were just getting lucky with this
working in some scenarios, but it fails quite cryptically on Python 3.8 on
macOS. Hopefully this should rectify the issue.

This reverts commit b9c98f1a. It seems the
__sync CAS built-ins are not implemented on dwords for arm64 and s390. So we end
up setting NEEDS_LIBATOMIC=True, but then still failing compilations. Here we
switch back to the old behaviour and also modify the NEEDS_LIBATOMIC test.

The Debian buildd logs for the last arm64 build [0] indicate that
NEEDS_LIBATOMIC was False, but later linking then failed with a missing
reference to __atomic_load16 and friends. I'm guessing this is something like
the x86 scenario, where only the __sync built-ins are capable of producing
inline code. Let's unconditionally use them on all platforms (not just x86 and
x86-64) and see if that resolves these issues.

  [0]: https://buildd.debian.org/status/fetch.php?pkg=rumur&arch=arm64&ver=2020.04.26-1&stamp=1588101624&raw=0

Github: related to #184 "debian: arm64 broken build"
Github: related to #185 "debian: armel broken build"

It is no longer possible to upgrade packages on FreeBSD 12.0 now that it is out
of support [0]. More information at [1, 2].

  [0]: https://www.freebsd.org/security/unsupported.html
  [1]: https://github.com/cirruslabs/cirrus-ci-docs/issues/632
  [2]: https://github.com/cirruslabs/cirrus-ci-docs/issues/625

Github: closes 138 "why does IsUndefined not inherit from UnaryExpr?"

Because the specific ordering of fields within a record or within a model is not
relied on, we now reorder these to try to optimise for performance of runtime
reads and writes during verification. Aligned hardware accesses are typically
faster than unaligned accesses, and we can avoid doing bit shifting in software
if we have a natural alignment. We try to approach the optimal here, but it is
essentially best effort.

Github: closes #147 "optimise record and state field ordering"

Apparently older versions of CMake do not like you using the "test" target as
they consider it reserved.

We were inadvertently taking a copy of the quantifier's decl's type, modifying
the copy, then discarding it. As a result, the tightening of the bounds on a
range would not take effect. The user-visible outcome of this was that the value
type logic would infer a larger C type than necessary to hold scalar values
(e.g. int64_t when it only needed int8_t).

Github: closes #181 "quantifier range refinement gets lost"

This lets us more easily force verbose output. This should help to address build
timeouts during Debian testing [0, 1, 2].

  [0]: https://buildd.debian.org/status/fetch.php?pkg=rumur&arch=mipsel&ver=2020.04.05-1&stamp=1587359957&raw=0
  [1]: https://buildd.debian.org/status/fetch.php?pkg=rumur&arch=armel&ver=2020.04.05-1&stamp=1587365346&raw=0
  [2]: https://lists.debian.org/debian-mentors/2020/04/msg00244.html

This isn't quite working and I can't see why right now. Debug this in future.

Github: closes #161 "Murphi preprocessor"

This reverts commit a9ae6f9c.

This GNU extension is rejected by some compilers when targeting C++11 with
-Werror=pedantic.

This case is actually handled naturally already.