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

Language.Copilot.Dispatch

Description

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.

Synopsis

Documentation

dispatch :: StreamableMaps Spec -> Sends -> 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 BackEnd Source

Constructors

Opts AtomToC 
Interpreter 

data AtomToC Source

Constructors

AtomToC 

Fields

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

triggers :: [(Var, String)]

A list of Copilot variable C function name pairs. The C funciton is called if the Copilot stream becomes True. The Stream must be of Booleans and the C function must be of type void foo(void).

arrDecs :: [(String, Int)]
 

data Interpreted Source

Constructors

Interpreted 
NotInterpreted 

type Iterations = IntSource

data Verbose Source

Constructors

OnlyErrors 
DefaultVerbose 
Verbose 

Instances