Acsl Annotation Assistant

ACSL Annotation Assistant

Generate comprehensive ACSL (ANSI/ISO C Specification Language) annotations for C/C++ programs to support formal verification with tools like Frama-C.

Core Capabilities

1. Function Contracts

Add complete function specifications with preconditions and postconditions:

/*@
  requires \valid(array + (0..n-1));
  requires n > 0;
  ensures \result >= 0 && \result  array[\result] >= array[i];
  assigns \nothing;
*/
int find_max_index(int *array, int n);

2. Loop Annotations

Generate loop invariants, variants, and assigns clauses:

/*@
  loop invariant 0  sum == \sum(0, k, array);
  loop assigns i, sum;
  loop variant n - i;
*/
for (i = 0; i  dest[i] == \old(src[i]);
  assigns dest[0..n-1];
*/
void memcpy_safe(char *dest, const char *src, size_t n);

4. Assertions and Assumptions

Insert runtime and verification assertions:

//@ assert 0  a[i]  sum(a, low, high) == sum(a, low, high-1) + a[high-1];
  }
*/

Annotation Workflow

Step 1: Analyze the Function

Before annotating:

• Identify inputs, outputs, and side effects
• Determine memory access patterns
• Understand algorithmic properties (sorting, searching, etc.)
• Note any implicit assumptions

Step 2: Add Function Contract

Start with the function-level specification:

1. Preconditions (requires): What must be true when function is called
2. Postconditions (ensures): What will be true when function returns
3. Assigns clause: What memory locations may be modified
4. Behavioral specification: Normal and exceptional behaviors if applicable

Step 3: Annotate Loops

For each loop, specify:

1. Loop invariant: Properties that hold before and after each iteration
2. Loop variant: Decreasing measure proving termination
3. Loop assigns: Memory modified within the loop

Step 4: Add Assertions

Insert intermediate assertions to:

• Document algorithmic properties
• Help verification tools
• Clarify complex logic

Step 5: Define Helper Predicates

Create reusable logical definitions for:

• Common patterns (sorted arrays, valid ranges)
• Domain-specific properties
• Complex mathematical relationships

Common ACSL Constructs

Memory Validity

\valid(ptr)                    // Single valid pointer
\valid(ptr + (low..high))      // Valid range
\valid_read(ptr)               // Read-only validity
\separated(ptr1, ptr2)         // No aliasing

Quantifiers

\forall type var; condition ==> property
\exists type var; condition && property

Logic Functions

\old(expr)                     // Value at function entry
\at(expr, Label)               // Value at specific point
\result                        // Function return value
\nothing                       // Empty set (for assigns)

Integer Ranges

\forall integer i; low  array[i] >= 0

Behaviors

/*@
  behavior valid_input:
    assumes n > 0;
    requires \valid(array + (0..n-1));
    ensures \result >= 0;

  behavior invalid_input:
    assumes n  0;
*/

/*@
  requires valid_array(array, n);
  ensures \result >= 0 && \result  array[\result] >= array[i];
  assigns \nothing;
*/
int find_max_index(int *array, int n) {
    int max_idx = 0;

    /*@
      loop invariant 0 
                     array[max_idx] >= array[k];
      loop assigns i, max_idx;
      loop variant n - i;
    */
    for (int i = 1; i  array[max_idx]) {
            max_idx = i;
        }
    }

    return max_idx;
}

Resources

This skill includes reference materials for ACSL:

references/

• acsl_reference.md - Comprehensive ACSL syntax reference
• common_patterns.md - Frequently used annotation patterns
• frama_c_integration.md - Tips for using with Frama-C

Load these references as needed for detailed syntax information or advanced patterns.

Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

• Author: ArabelaTso
• Source: ArabelaTso/Skills-4-SE
• License: Apache-2.0
• Homepage: https://ArabelaTso.github.io/Skills-4-SE/

Install and usage instructions live in the source repository linked above.