# Acsl Annotation Assistant

> Create ACSL (ANSI/ISO C Specification Language) formal annotations for C/C++ programs. Use this skill when working with formal verification, adding function contracts (requires/ensures), loop invariants, assertions, memory safety annotations, or any ACSL specifications. Supports Frama-C verification and generates comprehensive formal specifications for C/C++ code.

- **Type:** Skill
- **Install:** `agentstack add skill-arabelatso-skills-4-se-acsl-annotation-assistant`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [ArabelaTso](https://agentstack.voostack.com/s/arabelatso)
- **Installs:** 0
- **Category:** [Agent Skills](https://agentstack.voostack.com/c/agent-skills)
- **Latest version:** 0.1.0
- **License:** Apache-2.0
- **Upstream author:** [ArabelaTso](https://github.com/ArabelaTso)
- **Source:** https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/acsl-annotation-assistant
- **Website:** https://ArabelaTso.github.io/Skills-4-SE/

## Install

```sh
agentstack add skill-arabelatso-skills-4-se-acsl-annotation-assistant
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# 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:

```c
/*@
  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:

```c
/*@
  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:

```c
//@ 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
```c
\valid(ptr)                    // Single valid pointer
\valid(ptr + (low..high))      // Valid range
\valid_read(ptr)               // Read-only validity
\separated(ptr1, ptr2)         // No aliasing
```

### Quantifiers
```c
\forall type var; condition ==> property
\exists type var; condition && property
```

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

### Integer Ranges
```c
\forall integer i; low  array[i] >= 0
```

### Behaviors
```c
/*@
  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](https://github.com/ArabelaTso)
- **Source:** [ArabelaTso/Skills-4-SE](https://github.com/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.

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** no
- **Environment & secrets:** no
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/skill-arabelatso-skills-4-se-acsl-annotation-assistant
- Seller: https://agentstack.voostack.com/s/arabelatso
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.