C-rusted: The Advantages of Rust, in C, without the Disadvantages
Abstract
C-rusted is an innovative technology whereby C programs can be (partly) annotated so as to express: ownership, exclusivity and shareability of language, system and user-defined resources; dynamic properties of objects and the way they evolve during program execution; nominal typing and subtyping. The (partially) annotated C programs can be translated with unmodified versions of any compilation toolchain capable of processing ISO C code. The annotated C program parts can be validated by static analysis: if the static analyzer flags no error, then the annotations are provably coherent among themselves and with respect to annotated C code, in which case said annotated parts are provably exempt from a large class of logic, security, and run-time errors.
Keywords
Cite
@article{arxiv.2302.05331,
title = {C-rusted: The Advantages of Rust, in C, without the Disadvantages},
author = {Roberto Bagnara and Abramo Bagnara and Federico Serafini},
journal= {arXiv preprint arXiv:2302.05331},
year = {2023}
}
Comments
12 pages, 12 figures