David Pearce

z3-sys cannot find z3.h

3

Hey, So, following the docs it says to resolve this configure `Z3_SYS_Z3_HEADER` to the actual path. But, that doesn't seem to be resolving the issue. Here are my commands: ```...

Currently, the following passes verification: ```whiley assert (-6) / 4 == -2 assert (-6) % 4 == 2 ``` However, they _fail_ runtime checking! In contrast, the following pass runtime...

It makes sense that we have a single source of truth for the reference tests, since these are shared across multiple components. Currently, they are updated through manual copying ......

Improve MoveAnalysis Phase

1

_(see also #706)_ Currently, `MoveAnalysis` has two distinct limitations which should be addressed: 1. **Does not distinguish moves from borrows**. Consider the expression `arr[i]` for some array `arr`. The analysis...

Duplicate Error Messages

1

There are various situations where we can end up with _duplicate_ error messages. The following is a simple example: ```Whiley function f(int z) -> int: if z: return 1 return...

_(see also https://github.com/Whiley/RFCs/issues/36 and https://github.com/Whiley/RFCs/pull/51)_ The semantics of the runtime type test operator `is` remain problematic, despite potential improvements coming from RFC#51. **In short, relying only on the underlying type...

The following now fails to type check: ```Whiley type Tree is null | Node type Node is {int data, Tree rhs, Tree lhs} where (lhs is null) || (lhs.data <...

Subtyping for Explicit Casts

1

_(see also #845)_ At the moment, there is no sutyping operator for casts. Thus, the following fails: ```Whiley type Link is {int data} type BigLink is {int data, int code}...

The following does not parse for reasons unknown: ```Whiley type fn is function()->(int) method m(fn[] fs): assume fs[0]() == 11 ```

At the moment, the `branch always taken` check is embedded within `FlowTypeCheck`. This actually causes problems because it results in errors being raise prematurely. For example, consider this: ```Whiley method...