Project

General

Profile

« Previous | Next » 

Revision 9b0432bc

Added by Corentin Lauverjat over 1 year ago

  • ID 9b0432bc4c6c7165663ff1239ee93adac0a4a34d
  • Parent 9e88590e

Using deriving_ppx to derive show_ functions for the main types defined in lib/
Applying the same procedure of operator specialization taken from the C backend to Tiny
Lustrev has now a functional Tiny plugin : * -unrolling option has been renamed -duration because from an outside observer it is the length in steps of the abstract simulation * the plugin takes a JSON input file containing the bounds on input of the top node (option -bounds-input) * the plugins outputs its result in a Json format on the stdout. It can also output a {basename}_result.json file containing the result if the flag -tiny-output is provided
Adding a Tiny backend that generates Tiny code from Lustre
Repairing treatment of parsing error that was broken since transitioning from ocamlyacc to menhir

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