copilot-1.0: A stream DSL for writing embedded C monitors.



The Dispatch module : does all the IO, and offers an unified interface to both the interpreter and the compiler.

Also communicates with GCC in order to compile the C code, and then transmits the results of the execution of that C code. This functionnality is mostly used to check automatically the equivalence between the interpreter and the compiler. The Dispatch module only parses the command-line arguments before calling that module.



dispatch :: LangElems -> Vars -> BackEnd -> Iterations -> Verbose -> IO ()Source

This function is the core of Copilot : it glues together analyser, interpreter and compiler, and does all the IO. It can be called either from interface (which justs decodes the command-line argument) or directly from the interactive prompt in ghci. streams is a specification, inputExts allows the user to give at runtime values for the monitored variables. Useful for testing on randomly generated values and specifications, or for the interpreted version. be chooses between compilation or interpretation, and if compilation is chosen (AtomToC) holds a few additionnal informations. see description of BackEnd iterations just gives the number of periods the specification must be executed. If you would rather execute it by hand, then just choose AtomToC for backEnd and 0 for iterations verbose determines what is output.

data AtomToC Source




cName :: Name

Name of the C file to generate

gccOpts :: String

Options to pass to the compiler

getPeriod :: Maybe Period

The optional period

interpreted :: Interpreted

Interpret the program or not

outputDir :: String

Where to put the executable

compiler :: String

Which compiler to use

prePostCode :: Maybe (String, String)

Code to replace the default initialization and main

arrDecs :: [(String, Int)]
clock :: Maybe Clock

data Verbose Source