ACSL v1.23

Changes with respect to 1.22 include:

• add keywords related to pointer alignement (\aligned, alignof and _Alignof)
• clarify meaning of \valid, \valid_read and \initialized
• sections about memory have been reorganized

ACSL v1.22

Main change in this release is the removal of logic attributes, a mostly unused feature that is mostly superseded by C23's attributes.

ACSL v1.21

Changes with respect to 1.20 include:

• More precise definition of pre- and post- states of a function contract (fixes #49 and #70)
• Extend grammar for module definition and allow importing external symbols
• Default value of terminates clause is \false for functions with function specifier _Noreturn

ACSL v1.20

Main changes:

• Fix the default value for missing exits clauses (to \false).

ACSL v1.19

Main changes:

• add the \object_pointer and \pointer_comparable built-in predicates.

ACSL v1.18

Main change:

• clarifies meaning of terminates and decreases/variant clauses

ACSL v1.17

© 2021

ACSL v1.16

ACSL v1.16, target of Frama-C 22.0 Titanium.

ACSL v1.15

v1.15 of the ACSL manual

ACSL++ Manual v1.1

Merge pull request #64 from acsl-language/acslpp2

ACSL++ manual