sail/test/typecheck/pass/Replicate, branch sail2 Formal specification language for ISAs Update test error messages, hopefully will make Jenkins happy again 2020-04-28T19:45:21+00:00 Alasdair 2020-04-28T19:45:21+00:00 88fe9754f897d3d96533748c6fc73a2d8da76fec 






Update tests
2019-08-14T18:13:16+00:00

Thomas Bauereiss

2019-08-14T18:13:16+00:00

9a8746adb6c580880e3b94c2bcf6eaa4c99247a7












Merge remote-tracking branch 'origin/sail2' into separate_bv
2019-07-16T17:57:46+00:00

Alasdair Armstrong

2019-07-16T17:57:46+00:00

cd909e15b97739b10214023af04b2fbbb4d20cf7












Update test cases
2019-06-18T19:41:21+00:00

Thomas Bauereiss

2019-06-18T19:41:21+00:00

790da51af29e5a17f4bf0c8d95c9bbccb9747b41












Add well-formedness check for type schemes in valspecs.
2019-06-10T16:53:58+00:00

Brian Campbell

2019-06-10T16:53:58+00:00

3eadd260f7382f98eb7dcbd706a3ed3e910167eb

Fixes #47.
Also adjust the nexp substitution so that the error message points to a
useful location, and replace the empty environment with the initial
environment in a few functions that do type checking to ensure that the
prover is set up (which may be needed for the wf check).





Fixes #47.
Also adjust the nexp substitution so that the error message points to a
useful location, and replace the empty environment with the initial
environment in a few functions that do type checking to ensure that the
prover is set up (which may be needed for the wf check).







Experiment with making vector and bitvector distinct types
2019-05-17T17:38:35+00:00

Alasdair Armstrong

2019-05-17T17:38:35+00:00

a1ef7946b96d95b3192f8db496f09d4bb23b775a

Only change that should be needed for 99.9% of uses is to change
vector('n, 'ord, bit) to bitvector('n, 'ord), and adding

$ifndef FEATURE_BITVECTOR_TYPE
type bitvector('n, dec) = vector('n, dec, bit)
$endif

for to support any Sail before this

Currently I have all C, Typechecking, and SMT tests passing, as well
as the RISC-V spec building OCaml and C completely unmodified.





Only change that should be needed for 99.9% of uses is to change
vector('n, 'ord, bit) to bitvector('n, 'ord), and adding

$ifndef FEATURE_BITVECTOR_TYPE
type bitvector('n, dec) = vector('n, dec, bit)
$endif

for to support any Sail before this

Currently I have all C, Typechecking, and SMT tests passing, as well
as the RISC-V spec building OCaml and C completely unmodified.







Merge branch 'sail2' into smt_experiments
2019-05-07T14:10:09+00:00

Alasdair Armstrong

2019-05-07T13:56:39+00:00

61f9f9d7ee1e4113b960151b1521efcaddd037b0












Tidy up of div and mod operators (C implementation was previously inconsistent with ocaml etc.). Rename div and mod builtins to ediv_int/emod_int and tdiv_int/tmod_int and add corresponding implementations. Add a test with negative operands. This will break existing models but will mean users have to think about which versions they want and won't accidentally use the wrong one.
2019-03-22T16:55:23+00:00

Robert Norton

2019-03-22T16:50:48+00:00

f4acbce30be2aecdfc491478a24c5eb551824f24












Fix tests
2019-03-15T18:47:30+00:00

Thomas Bauereiss

2019-03-15T17:04:50+00:00

5222eb29434437190c83339602ca197a5cd6be7d












Do not store type synonyms as functions in the environment
2019-03-04T15:48:36+00:00

Alasdair Armstrong

2019-03-04T15:48:09+00:00

8efe97cd6d8140ebebf4d71e597f497dea385964