Project

General

Profile

Revision 9b0432bc README.md

View differences:

README.md
125 125
```
126 126
# frama-c -cpp-extra-args='-Iinclude'  filename.c
127 127
```
128
#### Tiny backend
129

  
130
The Tiny backend generates tiny (imperative) code from lustre. 
131
The example below generates tiny code for the node top of the two_counters.lus file
132

  
133
```
134
lustrec -d examples/two_counters -tiny -node top examples/two_counters/two_counters.lus
135
```
136

  
137
### Lustrev 
138

  
139
Lustrev is a Lustre verifier based on static analysis. 
140

  
141
#### Tiny verifier
142

  
143
With the option `-tiny` the verifier uses Tiny to analyse Lustre file. Tiny is based on theory of abstract interpretation. Set of values are represented as abstract values that overapproximate the values that can be taken by a variable.
144

  
145
This verifier runs an abstract simulation of the Lustre code. At each time step, the verifier outputs abstract values of the variable environnement.
146

  
147
It takes an Lustre file, a top node, a JSON file with the bounds on the parameters of the top node, and outputs a JSON file consisting of the abstract values of the variables at each time step.
148

  
149
The example below generates a two_counters_tiny.json file.
150
```
151
cd examples/two_counters
152
lustrev -node top -tiny -tiny-duration 5 -tiny-bounds-file tiny_input.json -tiny-output two_counters.lus 
153
```
154

  
128 155
### Ada backend 
129 156

  
130 157
Download ada from https://www.adacore.com/download

Also available in: Unified diff