Skip to content
Snippets Groups Projects
stady.md 979 B
Newer Older
---
layout: plugin
title: StaDy
description: Generation of test inputs confirming alarms generated by static analysis
key: derived
distrib_mode: free
repo_url: https://github.com/gpetiot/Frama-C-StaDy
---

## Overview

**StaDy** is dedicated to confirm that an alarm generated by [Eva](eva.html) or
an annotation marked as Unknown by [WP](wp.html) is indeed a real issue.
This is done by trying to have [PathCrawler](pathcrawler.html) generate
a test case that will invalidate the corresponding annotation.

## Usage

[StaDy]({{page.repo_url}}) is available as a separate open-source plug-in.
However, it relies on the [Pathcrawler](pathcrawler.html) plug-in,
which itself is not publicly available.

Once installed, it will be activated by the `-stady` option.
Annotations that are found to be violated by some test input will be marked
as `invalid` (i.e. appear with a red bullet on the GUI).

## Dependencies

**StaDy** depends on the [PathCrawler](pathcrawler.html) plug-in.