文章基本信息

标题：Embedded Program Annotations for WCET Analysis
本地全文：下载
作者：Bernhard Schommer ; Christoph Cullmann ; Gernot Gebhard 等
期刊名称：OASIcs : OpenAccess Series in Informatics
电子版ISSN：2190-6807
出版年度：2018
卷号：63
页码：1-13
DOI：10.4230/OASIcs.WCET.2018.8
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We present __builtin_ais_annot(), a user-friendly, versatile way to transfer annotations (also known as flow facts) written on the source code level to the machine code level. To do so, we couple two tools often used during the development of safety-critical hard real-time systems, the formally verified C compiler CompCert and the static WCET analyzer aiT. CompCert stores the AIS annotations given via __builtin_ais_annot() in a special section of the ELF binary, which can later be extracted automatically by aiT.
关键词：Worst-Case Execution Time (WCET) Analysis; Annotation Support; CompCert; Tool Coupling; aiT