Under-approximating Memory Abstractions - Sorbonne Université
Preprints, Working Papers, ... Year : 2024

Under-approximating Memory Abstractions

Abstract

This work presents a sound backward analysis for sufficient pre-conditions inference in C programs, by abstract interpretation. It utilizes the under-approximation abstract operators studied by Milanese and Miné for a purely numeric subset of C, and extends them to support the C memory model. Pointer dereferences are handled with the cell abstraction and dynamic memory allocations with the re- cency abstraction. A direct usage of the abstract operators proposed in these previous works in an under-approximation framework is not possible as either internally they rely on over-approximated operators (e.g., cell removal) or an extension to this framework is not straightforward (e.g., under-approximating join). In this work we propose new operators that are under-approximating, and on top of this we design a backward semantics. The analysis is implemented in the MOPSA analyzer and its performance is assessed in detection of sufficient pre-conditions for runtime errors in 13,261 C tasks from NIST Juliet test suite.
Fichier principal
Vignette du fichier
samplepaper.pdf (5.4 Mo) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-04670146 , version 1 (11-08-2024)

Identifiers

  • HAL Id : hal-04670146 , version 1

Cite

Marco Milanese, Antoine Miné. Under-approximating Memory Abstractions. 2024. ⟨hal-04670146⟩
143 View
74 Download

Share

More