sail/test/isabelle, branch sail2 Formal specification language for ISAs tests: Move copy-pasted code into a shared helper .sh 2020-09-25T11:30:09+00:00 Alex Richardson 2020-09-25T09:12:56+00:00 782d3860eb0134c81d4a4204b7caab72cda3bd1d Also fix a few shellcheck warnings related to printf while doing so. 
Also fix a few shellcheck warnings related to printf while doing so.
Pass Lem library path to Isabelle 2019-01-21T23:16:47+00:00 Thomas Bauereiss 2019-01-21T23:16:47+00:00 365cf2015c77551e37d31336220497f6ca84794c 






Don't require manual set up of Isabelle session directories
2019-01-21T20:07:20+00:00

Thomas Bauereiss

2019-01-21T19:53:59+00:00

aeb0f82f67ff829cd7a4b57c638b44a07d39ba3b

Since Isabelle 2018, specifying the same directory both on the command
line and persistently in the user's ROOTS file is allowed, so we don't
have to choose between one or the other any more.





Since Isabelle 2018, specifying the same directory both on the command
line and persistently in the user's ROOTS file is allowed, so we don't
have to choose between one or the other any more.







Update CHERI code extraction from Isabelle
2018-07-10T23:19:52+00:00

Thomas Bauereiss

2018-07-10T21:39:23+00:00

63fccf3902edbeb7816e6c419b0cbdcfea423cb9

Also use zero-initialised memory.  Apparently some tests access unitialised
memory, and the default behaviour of the Lem shallow embedding is to fail in
this case.





Also use zero-initialised memory.  Apparently some tests access unitialised
memory, and the default behaviour of the Lem shallow embedding is to fail in
this case.







Update CHERI code generation from Isabelle
2018-07-09T13:47:49+00:00

Thomas Bauereiss

2018-07-07T21:47:57+00:00

5d862dc23d4641a0e7d89cd747bc2ba4007ee8f5












Simplify treating of undefined_bool in Lem library
2018-07-09T13:38:51+00:00

Thomas Bauereiss

2018-06-22T18:03:02+00:00

edc2be164fcf53c333796e55b93f94bf6c9ed152

Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state.  The previous behaviour can be
implemented as Sail code, if desired.

Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.





Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state.  The previous behaviour can be
implemented as Sail code, if desired.

Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.







Clean out old sequential files
2018-05-17T15:38:26+00:00

Brian Campbell

2018-05-17T15:37:47+00:00

f5672ea6a1e04ad1f2bee91ad86584b183d323b4












Fix Isabelle->OCaml wrapper
2018-05-17T14:31:11+00:00

Thomas Bauereiss

2018-05-17T14:31:11+00:00

3af9f9dfda3972f485cd98b2a2d110c16325b3a3












Add Isabelle code generation for sequential CHERI model
2018-05-11T13:23:43+00:00

Thomas Bauereiss

2018-05-11T13:23:43+00:00

5089d9ec81303ce50992084368d3d35f7169d230












Adapt Isabelle code generation to Byte_sequence changes
2018-05-09T15:50:57+00:00

Thomas Bauereiss

2018-05-09T15:50:57+00:00

86f7649e6b6cc00ea1d73a59d25d4bc4938ae1f5