# Changeset 3668

Ignore:
Timestamp:
Mar 16, 2017, 7:39:56 PM (8 days ago)
Message:

Attention on FramaC plugin section, now

File:
1 edited

Unmodified
Added
Removed
• ## Papers/jar-cerco-2017/framac.tex

 r3661 \label{sect.framac.plugin} The Cost plug-in for the Frama-C platform has been developed in order to automatically synthesize the cost annotations added by the CerCo compiler on a C source program into assertions of the WCET of the functions in the program. The architecture of the plug-in is depicted in figure 3. It accepts a C source file as a parameter and creates a new C file that is the former with additional cost annotations (C code) and WCET assertions (ACSL annotations).  First, the input file is fed to Frama-C that will in turn send it to the Cost plug-in. The action of the plug-in is then: In this section we discuss the CerCo FramaC plugin. The plugin is able to automatically synthesise cost annotations inferred by the CerCo C compiler into assertions capturing the Worst Case Execution Time (WCET) of the functions in the program. We will first briefly discuss the design and implementation of the plugin, before turning our attention to its use in a case study. This case study will use the CerCo FramaC plugin to compute the WCETs of a selection of programs written in Lustre, a synchronous dataflow language. \subsection{Plugin design considerations, and ruminations on soundness} \label{subsect.plugin.design} The CerCo FramaC plugin accepts a C source file as input and outputs a new C file, which is a modified copy of the input with additional cost annotations (C code) and WCET assertions (ACSL annotations) inserted. At a high-level of abstraction, the FramaC plugin works by: \begin{enumerate} \item apply the CerCo compiler to the source file; \item synthesize an upper bound of the WCET of each function of the source program by reading the cost annotations added by CerCo; \item   add the results in the form of post-conditions in ACSL format, relating the cost of the function before and after its execution. \item First applying the CerCo compiler to the source file, obtaining a modified C source file with cost annotations automatically inserted by the CerCo compiler, \item Synthesising an upper bound of the WCET of each function of the source program by reading the cost annotations added by CerCo; \item Further modifying the C source file, by adding WCET annotations in the form of ACSL post-conditions, which relate the cost of the function before and after its execution, \item Finally, outputting this final file. \end{enumerate}
Note: See TracChangeset for help on using the changeset viewer.