Changeset 3668


Ignore:
Timestamp:
Mar 16, 2017, 7:39:56 PM (3 months ago)
Author:
mulligan
Message:

Attention on FramaC plugin section, now

File:
1 edited

Legend:

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

    r3661 r3668  
    77\label{sect.framac.plugin}
    88
    9 The Cost plug-in for the Frama-C platform has been developed in order to
    10 automatically synthesize the cost annotations added by the CerCo compiler on a
    11 C source program into assertions of the WCET of the functions in the program.
    12 The architecture of the plug-in is depicted in figure 3. It accepts a C source
    13 file as a parameter and creates a new C file that is the former with additional
    14 cost annotations (C code) and WCET assertions (ACSL annotations).  First, the
    15 input file is fed to Frama-C that will in turn send it to the Cost plug-in.
    16 The action of the plug-in is then:
    17 
     9In this section we discuss the CerCo FramaC plugin.
     10The 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.
     11We will first briefly discuss the design and implementation of the plugin, before turning our attention to its use in a case study.
     12This case study will use the CerCo FramaC plugin to compute the WCETs of a selection of programs written in Lustre, a synchronous dataflow language.
     13
     14\subsection{Plugin design considerations, and ruminations on soundness}
     15\label{subsect.plugin.design}
     16
     17The 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.
     18At a high-level of abstraction, the FramaC plugin works by:
    1819\begin{enumerate}
    19         \item apply the CerCo compiler to the source file;
    20         \item synthesize an upper bound of the WCET of each function of the source
    21                 program by reading the cost annotations added by CerCo;
    22         \item   add the results in the form of post-conditions in ACSL format,
    23                 relating the cost of the function before and after its execution.
     20\item
     21First applying the CerCo compiler to the source file, obtaining a modified C source file with cost annotations automatically inserted by the CerCo compiler,
     22\item
     23Synthesising an upper bound of the WCET of each function of the source program by reading the cost annotations added by CerCo;
     24\item
     25Further 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,
     26\item
     27Finally, outputting this final file.
    2428\end{enumerate}
    2529
Note: See TracChangeset for help on using the changeset viewer.