Changes between Version 46 and Version 47 of Language

Timestamp:

05/22/23 10:47:22 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -795 +795 @@
 Function contracts can be specified as annotations---formatted comments---preceding a function prototype or definition.
 The language for these annotations is based on the specification language [https://frama-c.com/html/acsl.html ACSL] used by Frama-C.
-The high-level syntax is
+A translation unit must include the following pragma to inform CIVL that it should parse the ACSL annotations in that translation unit:
+{{{
+#pragma CIVL ACSL
+}}}
+If this line is not present, the annotations will be ignored.
+
+The high-level syntax for a procedure contract is
 
   `/*@` ''clause''* `*/`