WhileyCompiler
WhileyCompiler copied to clipboard
Whiley
The Whiley Compiler (WyC)
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 ......
When using the following comment structure (that enables to switch commented lines easily), ```Whiley function comments(int a, int b) -> int: //* a = a + 1 /*/ b =...
_(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...
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 <...
_(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...