Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Problem with type aliases in SMT backend using version 0.15 #187

Closed
rmn30 opened this issue Nov 24, 2022 · 2 comments
Closed

Problem with type aliases in SMT backend using version 0.15 #187

rmn30 opened this issue Nov 24, 2022 · 2 comments

Comments

@rmn30
Copy link
Contributor

rmn30 commented Nov 24, 2022

default Order dec

$include <arith.sail>
$include <vector_dec.sail>

type r1 = range(0, ((2 ^ 32) - 1))

function foo (x : bits(32)) -> r1 = {
    unsigned(x)
}

$property
function prop (x : bits(32)) -> bool = {
    foo(x) == 0
}

Compiling the above file with sail -smt produces an error:

Type error:
test.sail:8.13-33:
8 |function foo (x : bits(32)) -> r1 = {
  |             ^------------------^
  | . range(0, (2 ^ 32 - 1)) and . r1 do not match between function and val spec

If you substitute the type alias manually the error goes away.

@rmn30
Copy link
Contributor Author

rmn30 commented Nov 24, 2022

I should also note that the error is new in version 0.15 and that it does not occur with the C backend.

@bacam bacam closed this as completed in 16d5461 Nov 24, 2022
@rmn30
Copy link
Contributor Author

rmn30 commented Nov 25, 2022

Thanks!

avsm pushed a commit to ocaml/opam-repository that referenced this issue Aug 30, 2023
…_manifest, sail_lem_backend, sail_latex_backend, sail_doc_backend, sail_coq_backend, sail_c_backend, sail and libsail (0.16)

CHANGES:

##### New documentation backend

A new documentation backend for integrating with Asciidoctor has been
added.

##### Automatic formatting (EXPERIMENTAL)

The `sail -fmt` option can be used to automatically format Sail
source. This currently misses some features and can produce ugly
output in some known cases, so is not ready for serious usage yet.

##### Fixes

Various bugfixes including:

* Issue 203: rems-project/sail#203
* Issue 202: rems-project/sail#202
* Issue 188: rems-project/sail#188
* Issue 187: rems-project/sail#187
* Issue 277: rems-project/sail#277

Various mapping issues such as:

* Issue 244: rems-project/sail#244

As well as other minor issues

The `val cast` syntax and support for implict casts is now entirely
removed, as mentioned in the previous release changes. The flags are
still allowed (to avoid breaking Makefiles) but no longer do anything.

The pattern completeness checker has been improved and is now context
sensitive in some cases.
nberth pushed a commit to nberth/opam-repository that referenced this issue Jun 18, 2024
…_manifest, sail_lem_backend, sail_latex_backend, sail_doc_backend, sail_coq_backend, sail_c_backend, sail and libsail (0.16)

CHANGES:

##### New documentation backend

A new documentation backend for integrating with Asciidoctor has been
added.

##### Automatic formatting (EXPERIMENTAL)

The `sail -fmt` option can be used to automatically format Sail
source. This currently misses some features and can produce ugly
output in some known cases, so is not ready for serious usage yet.

##### Fixes

Various bugfixes including:

* Issue 203: rems-project/sail#203
* Issue 202: rems-project/sail#202
* Issue 188: rems-project/sail#188
* Issue 187: rems-project/sail#187
* Issue 277: rems-project/sail#277

Various mapping issues such as:

* Issue 244: rems-project/sail#244

As well as other minor issues

The `val cast` syntax and support for implict casts is now entirely
removed, as mentioned in the previous release changes. The flags are
still allowed (to avoid breaking Makefiles) but no longer do anything.

The pattern completeness checker has been improved and is now context
sensitive in some cases.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant