Pre-release Notes

This page logs recent changes and updates made for Cyclone pre-release.

Version 1.10.1220 (0726) - [09-December-2024]

• Fix issue: division equal operator casts real to int.
• Fix issue: local variables cannot be updated in function.
• Fix issue: local variables cannot be initialized appropriately in function.
• Fix issue: function in assertion throws null exception.
• Fix issue: workflow on local workstation.
• Update: update solver to 4.13.0
• Update: update test oracles with more sample problems (bv).
• Update: update prefix notation for bv.

Version 1.09.1182 (0717) - [25-June-2024]

• New feature: add bv (bit-vector) data type to primitive type and bitwise operations (+,-,*,/,%,and,or,xor,left/right shift,negation) are supported.
• Update: new frame condition generation.
• Update: add bv test cases to the test oracle.
• Update: display bv values in the trace.
• Update: restructure graph condition engine to support bv.
• Fix issue: Assigning an enum constant to primitive data types throws run-time error.
• Fix issue: display message about the checking bound is exceeding 2^32-1.
• Fix issue: initializing variables using functions and assertion using functions.

Version 1.08.873 (0708) - [05-March-2024]

• Update: all tutorial examples are used standard graph keywords
• Fix issue: a crash occur when generating trace on fresh variables.
• Fix issue: a boolean variable is a valid statement inside a node.
• Fix issue: file separator is wrongly interpreted on Windows.

Version 1.08.848 (0708) - [01-January-2024]

• Update: graph-based trace contains labels
• Update: redirect stderr to stdout
• Update (CI): reschedule clean bot
• Update (CI): remove redundant specs in the benchmark
• Update (Solver): update solver to 4.12.4
• Fix issue: a crash in node modifiers (abstract and normal)
• Fix issue: incorrect condition generation for local invariant
• Fix issue: a crash in let expression

Version 1.08.801 (0699) - [04-August-2023]

• Update: compiler can now detect arm64 (M1/M2)
• Update: more examples (from TLA,leetcode) are added into benchmark
• Update: compiler displays different messages
• New feature: add power operator (**) for int and real
• Fix issue: trance generation on windows platform (test oracle)
• Fix issue: mixing result of unknown and no path(counter-example) found.

Version 1.08.757 (0696) - [30-June-2023]

• New feature: add exclusion list for edge operator: *, + and ->
• New feature: add shorthand edge creation
• Fix issue: when a trace is failed to generate, additional messages are provided
• Fix issue: version number display
• Fix issue: pre-release workflows pack wrong examples
• Fix issue: testing oracles fail to generate trace on Windows platform
• Fix issue: VC engine generates wrong vc using non-english locale
• Update: trace filename now always matches source filename

Version 1.08.688 (0690) - [19-May-2023]

• Fix issue: crash of using enum data types.
• Update: benchmark for cyclone.
• Update: solver libraries.
• Update: Cyclone4Web.
• New feature: Cyclone native IDE (Experimental)

Version 1.07.685 (0686) - [17-Feb-2023]

• Fix issue: precision for real data type.
• Fix issue: modulo operator does not work with invariant.
• Fix issue: occurrence path operator produces wrong path conditions.
• Update: ubuntu-22.04 for CI.
• Update: sublime package.
• Update: add more sample problems (neural network,coffee can, einsteins riddle.).
• Update: solver libraries.
• New feature: Cyclone VS Code Plug-in (Experimental)
• New feature: Cyclone4Web (Experimental)

Version 1.07.682 (0686) - [06-Jan-2023]

• Fix issue of file path in trace generator.
• Change compiler interface: show full path of generated trace.
• Update solvers libraries (x86).

Version 1.07.680 (0686) - [17-Dec-2022]

• Fix issue of shorthand operators used in composite expressions
• Fix issue of enum data type assignment (integer value is not allowed now).
• Fix issue of return statement used in node/state.
• Fix coverage workflow crash issue.
• Users can now use --nocolor to disable color output in Mac & Linux.
• Change the compiler's return values in the test oracles.
• Remove redundant grammar rules.
• More parser & semantics testing scenarios are added into test & coverage workflow.
• Fix multiple other minor issues.

Version 1.07.675 (0686) - [02-Dec-2022]

• Add function support (experimental).
• Fix issue of << operator error when the length is set to 1.
• Update solver libraries.

Version 1.06.654 (0654) - [21-Oct-2022]

• Enumeration is now categorized as Mode.
• Update solver libraries

Version 1.06.653 (0652) - [07-Oct-2022]

• Fix issue of generating trace files (.trace) when enumeration mode is enabled.
• Fix a few minor issues about trace generation.
• Add a local test workflow machine.

Version 1.06.653 (0651) - [23-Sept-2022]

• Anonymous edge now can be used for a single transition.
• Update solver libraries - version:4.11.2.0

Version 1.06.652 (0650) - [09-Sept-2022]

• Users now can choose specific invariants to verify.
• Add an exclusion list for any one path operator.
• Fix wrong type error messages emitted by compiler.
• Fix mix use of void and undefined type for type checking.
• Fix issue of handling prefix minus sign for expressions.
• Fix issue of logging errors.

Version 1.05.650 (0646 Ulysses) - [26-Aug-2022]

• This is a special build for thanking Ulysses funding scheme.
• Fix issue of deleting conditions when compiler throws exceptions.
• Fix issue of generating wrong conditions of multiple invariants .
• Fix multiple minor issues
• Update test oracles in CI (add concurrency category).

Version 1.05.649 (0632) - [19-Aug-2022]

• Add a new trace output format (option-output="dot"). Support dot file generation. Use Graphviz to produce image-based trace.
• Update build scripts to support png file generation (Graphviz installation is required).
• Update CI and png files can be downloaded as trace files.

Version 1.05.647 (0591) - [12-Aug-2022]

• Add annotation @label support to track an assertion for inconsistent detection.
• Fix stack overflow issue when length is too large.
• Update x86 solver's libraries (V.4.10.2).
• Add a switch (--color) to enable color output on Powershell/Windows Terminal/Cmd (ANSI colors must be enabled)

Version 1.05.642 (0584) - [05-Aug-2022]

• Add a new feature (experimental): inconsistent detection for invariants. Use option-detect=true; to enable it.
• Allow record data type to be used in conditional transition.
• Catch out of memory error when condition size exceeds JVM memory size.
• Update solver lib - resolve version number problem in Linux pre-release.

Version 1.05.639 (0581) - [29-July-2022]

• Fix initial keyword cannot refer record data type.
• Update solver with new libraries.
• Include a pre-release version for ARM64 (M1/M2).

Version 1.05.638 (0580) - [22-July-2022/post-France]

• Trace generator now generates variables based on their alphabetical order.
• Update solver with new libraries.

Version 1.05.638 (0579) - [01-July-2022]

• Fix compiler crash on command: check upto 1.
• Fix trace generator crashes when variables that have the same name as field in record data type.
• Fix wrong sequence of AST generation of variable declaration.
• Fix enum data type in a record cannot be bound to != operator.

 

More changes, updates and fixes, see here.

 

 

---

@2020-2024 Hao Wu. All rights reserved. Last update: 09-December-2024