Known issues of the compiler

[alastairreid]

We know about the following limitations of the compiler

Missing features that we do not plan to address

• No string operations are supported so the only strings you can use are string literals.
  We strongly encourage limiting the use of strings to logging/debugging prints.
• The real type, real literals and real operations are not supported.
  These are only used in floating point specs and we plan to release a floating point specification that avoids the use of 'real'.

Missing features that we do plan to address

• Bitvectors are only supported if is is possible to determine the bitwidth based on how the function that uses it is used.
  We currently work around this by inserting case-splits manually (or in machine generated code like instruction decoders). This could be improved by automatically inserting case-splits.
• Runtime checks are not performed for array indexes and bitvector slices. (Missing ASL feature: runtime checks #32)
• Integers are represented by a fixed bitwidth (usually 128 bits) which makes it possible that integers will overflow or wraparound. (Bug: Fixed width integer representation #36)

Scope for improvement / optimization

• Generated code often contains dead code such as local variables that are not used (Spurious warning messages in generated code #33)
• Changing runtime library changes the types of imported/exported functions - this makes it hard to write code that works for any runtime library (Fixed by New Foreign Function Interface (FFI) #25)