< Retour au sommaire

Frama-C/Eva as a debugger engine through the Debug Adapter Protocol (DAP)

Jules Massart le

Lieu: Salle 1073

Suivre en visio

Abstract

The Eva Abstract Debugger is an interactive tool built on top of the Eva plugin in Frama-C. It provides a debugger-like interface, integrated as a VSCode extension, to help developers explore static analysis results more intuitively. The tool allows users to step through abstract execution, inspect variable domains, set and manage breakpoints, and explore multiple abstract states when needed. Features like branch selection at conditionals and support for adding annotations on the fly aim to make static analysis more practical and accessible.

To support dynamic branch selection, the tool replaces the traditional Weak Topological Order (WTO) with a new iteration strategy based on a Weak Partial Order (WPO). This generalizes Bourdoncle’s algorithm by allowing a partial, rather than total, ordering of nodes. While currently used to control the order in which branches are explored, this approach could be extended in the future to enable parallel exploration of branches using multiple threads, improving analysis speed.

The goal is to assist users in better understanding the possible behaviors of their programs through static analysis.