We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

Proof of Pointer Programs with Ownership in SPARK

Formale Metadaten

Titel
Proof of Pointer Programs with Ownership in SPARK
Serientitel
Anzahl der Teile
561
Autor
Lizenz
CC-Namensnennung 2.0 Belgien:
Sie dürfen das Werk bzw. den Inhalt zu jedem legalen Zweck nutzen, verändern und in unveränderter oder veränderter Form vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen.
Identifikatoren
Herausgeber
Erscheinungsjahr
Sprache

Inhaltliche Metadaten

Fachgebiet
Genre
Abstract
Pointers are a notorious "defect attractor", in particular when dynamic memory management is involved. Ada mitigates these issues by having much less need for pointers overall (thanks to first-class arrays, parameter modes, generics) and stricter rules for pointer manipulations that limit access to dangling memory. Still, dynamic memory management in Ada may lead to use-after-free, double-free and memory leaks, and dangling memory issues may lead to runtime exceptions. The SPARK subset of Ada is focused on making it possible to guarantee properties of the program statically, in particular the absence of programming language errors, with a mostly automatic analysis. For that reason, and because static analysis of pointers is notoriously hard to automate, pointers have been forbidden in SPARK until now. We are working at AdaCore since 2017 on including pointer support in SPARK by restricting the use of pointers in programs so that they respect "ownership" constraints, like what is found in Rust. In this talk, I will present the current state of the ownership rules for pointer support in SPARK, and the current state of the implementation in the GNAT compiler and GNATprove prover, as well as our roadmap for the future.