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 < n;
  ensures \forall integer i; 0 <= i < n ==> 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 <= i <= n;
  loop invariant \forall integer k; 0 <= k < i ==> sum == \sum(0, k, array);
  loop assigns i, sum;
  loop variant n - i;
*/
for (i = 0; i < n; i++) {
    sum += array[i];
}

3. Memory Safety Specifications

Add pointer validity and separation annotations:

/*@
  requires \valid(dest + (0..n-1));
  requires \valid_read(src + (0..n-1));
  requires \separated(dest + (0..n-1), src + (0..n-1));
  ensures \forall integer i; 0 <= i < n ==> 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 <= index && index < array_length;
//@ assume divisor != 0;

5. Axiomatic Definitions and Predicates

Define reusable logical predicates and axioms:

/*@
  predicate sorted{L}(int *a, integer n) =
    \forall integer i, j; 0 <= i <= j < n ==> a[i] <= a[j];
*/

/*@
  axiomatic Sum {
    logic integer sum{L}(int *a, integer low, integer high);

    axiom sum_empty{L}:
      \forall int *a, integer i; sum(a, i, i) == 0;

    axiom sum_next{L}:
      \forall int *a, integer low, high;
        low < high ==> 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