A couple of weeks ago, Travis CI upgraded their default Linux environment from
Ubuntu Trusty 14.04 to Ubuntu Xenial 16.04 [0]. Clang 5 and 6 builds started
failing because the llvm-toolchain repositories we're using don't support
Xenial. I suspect other Clang builds that are passing (e.g. Clang 4) are only
doing so coincidentally. I didn't investigate the failures initially, assuming
they were yet another transient Travis failure, and when I did it was
surprisingly hard to find the answer [1].

The fix in this commit is to pin these builds to Trusty. In future we should
also (1) pin the other Linux builds and (2) extend testing to Xenial.

  [0]: https://changelog.travis-ci.com/xenial-as-the-default-build-environment-99476
  [1]: https://travis-ci.community/t/cannot-apt-get-install-clang-5-0/3250/3

Now instead of ending with a messy Python trace and leaving the temporary
directory behind, we clean up nicely. We don't bother catching all signals or
attempt to do this fully robustly. This is just for the common scenario of a
long running checker that the user interrupts.

We were using the sigsetjmp()/siglongjmp() exception mechanism when either of
two things were true:

  1. --max-errors > 1; or
  2. the model has assumptions.

As of 7dda1203, a failed assumption is signalled
via a normal return value, not via a siglongjmp(). As a result, we no longer
need to require a jmp_buf in this case. This should result in a slight speed up
for models that have assumptions but run with --max-errors < 2.

Github: related to #127 "--max-errors > 1 produces unsafe code"

The motivation for this change is to fix an error in our usage of sigsetjmp().
When using jmp_bufs (JMP_BUF_NEEDED), we use sigsetjmp() and siglongjmp() to
give us an exception-handling-like mechanism to jump back to the exploration
loop after signalling an error. This pattern is fine except that these calls are
documented to leave all non-volatile locals in an indeterminate state. We had
several of these that were important (e.g. the pointer to the state that we go
on to free).

My initial planned solution to this was to simply mark the relevant variables
volatile. However, this comes with some drawbacks. Unconditionally marking these
volatile impedes the compiler's optimiser in the case when we're not using
jmp_bufs, while conditionally marking them volatile overcomplicates the code
generation logic. To further complicate this, some of the relevant variables are
generated (ruleset iterators). We would have to cast away these variables'
volatility when passing them to rules which would introduce even further
complications.

Instead, we duplicate the sigsetjmp() calls and move them inwards. E.g. for
guards, we call sigsetjmp() as the first step in the guard itself and then use
the return value of the guard to indicate to the exploration loop whether
siglongjmp() was called. The advantage of this is that the only work done in the
siglongjmp() path is now returning from the containing function; there are no
longer any relevant non-volatile locals.

This had a couple of unanticipated side effects:

  1. The error call in case of a deadlock had to be moved into its own function
     to also avoid having any non-volatile locals. This is not a problem, just
     unexpected.
  2. Return statements now awkwardly return a boolean when they have no
     associated expression. Relatedly void-returning functions (procedures) now
     have a boolean return type. This is because a return statement can be used
     in a rule (which now returns a boolean). We could have done something more
     elaborate like have an empty return statement jump to the end of the
     rule/function, but it seemed this would be more likely to confuse the
     compiler.

Github: closes #127 "--max-errors > 1 produces unsafe code"

Github: related to #128 "negative literals are not taken into account when
determining value type"

Github: closes #128 "negative literals are not taken into account when
determining value type"

Github: related to #128 "negative literals are not taken into account when
determining value type"

Github: related to #126 "--counterexample-trace off produces code that does not
compile"

This fixes a compile error resulting from bad code generation when
counterexample traces are disabled and there are no liveness properties.

Github: closes #126 "--counterexample-trace off produces code that does not
compile"

Github: related to #126 "--counterexample-trace off produces code that does not
compile"

The previous pointer is used during liveness checks, but we failed to notice
that it is only defined when counterexample traces are enabled. We now enable it
if either of these features are in use.

Github: related to #126 "--counterexample-trace off produces code that does not
compile"

We're going to need to start using it at preprocessor time.

Github: related to #126 "--counterexample-trace off produces code that does not
compile"

Github: related to #126 "--counterexample-trace off produces code that does not
compile"

Github: related to #126 "--counterexample-trace off produces code that does not
compile"

Github: related to #125 "diff traces over share with arrays"

When printing a diff counter-example trace (the default), some values that did
not change were being re-printed. That is, sometimes there would be no delta in
the value of a state component between one state and the next but its value
would be printed anyway. The underlying problem was that the handle used to read
from the previous state was incorrect. More specifically, this handle was always
using a base value of the start of the state data rather than the byte in which
the current field started.

This bug was introduced in d783655e when state
handles were changed to use a closer base. We missed that this left the
calculation of the handle to the previous state in state_print incorrect.

Github: closes #125 "diff traces over share with arrays"

Github: related to #125 "diff traces over share with arrays"

These were included originally because the thinking was that we would eventually
have command line options allowing the user to change the types of individual
properties. In this scheme, one of the possibilities would be "disable this
property." Now that all the planned property types are implemented (invariants,
covers, and liveness) it's become clear that changing the type of a property
after it's been written isn't something you generally want to do. Moreover, if
you really do want to do this it's unlikely something you need to be tweakable
from the command line; you can just go into the model source and edit the
relevant property.

Note that a side effect of this change is that 'property' is no longer a
keyword.

Github: closes #47 "properties, covers, etc"

Thanks to suggestions from Yann Collet in
https://fastcompression.blogspot.com/2019/01/compiler-warnings.html.

I didn't realise that COMPILE_FLAGS is not an additive property and setting it
the way we were doing wipes out its previous value. In the case where the
compiler supports both these flags, the setting of -Wno-register was causing
-Wno-sign-compare to be lost and thus become re-enabled by the preceding -Wall.

Why do I always fail to get RST right the first time?

To reflect that we'll start documenting some more things than data structures in
this series.

This change effectively pre-assigns people to houses. There was no need to model
this decision within the exploration of the model itself because nothing is
known about the people at the time they are assigned to houses, so this still
leaves the entire problem space open.

This model is still not checkable within 16GB, so it may be an interesting test
case to use for work on compressed representations.

We don't use it and this opens the way to more aggressive sandboxing of the
remaining I/O streams (stdout and stderr) should we want to.

In this case, the negation does not overflow the representation. Of course what
it means to negate an unsigned integer is debatable but I'm not going to prevent
you doing it.

Github: related to #23 "Use native scalars of variable size"

We need to start discriminating between value_to_string and raw_value_to_string
and this is the path that gets us there. As an additional bonus, this likely
accelerates checking in the cases when tracing is enabled.

Github: related to #23 "Use native scalars of variable size"

To be used in future for handle_read_raw and handle_write_raw.

Github: related to #23 "Use native scalars of variable size"

Github: related to #23 "Use native scalars of variable size"

The thinking here is to find a type that we can use as the result of
handle_read_raw and input to handle_write_raw.

Github: related to #23 "Use native scalars of variable size"