Project

General

Profile

Download (2.24 KB) Statistics
| Branch: | Tag: | Revision:
1
Current status : [![Build Status](https://travis-ci.org/coco-team/lustrec.svg?branch=master)](https://travis-ci.org/coco-team/lustrec)
2

    
3
# About LustreC
4

    
5
LustreC is a modular compiler of Lustre code into C and Horn Clauses.
6

    
7
# Dependencies
8

    
9
```
10
export LD_LIBRARY_PATH="$(ocamlfind query z3):$LD_LIBRARY_PATH"
11
```
12

    
13
## On a fresh ubuntu/debian-like install
14
```
15
> apt-get install opam libmpfr-dev
16
```
17
Get a fresh version of ocaml
18
```
19
> opam switch 4.06.1
20
```
21
Install some dependencies
22
```
23
> opam install depext ocamlgraph mlmpfr num cmdliner fmt logs yojson menhir
24
```
25
In OSX, some issues with Z3, please pin the following version:
26
```
27
> opam pin add z3 4.8.1
28
> opam install z3
29
```
30

    
31
## On Mac
32
brew install autoconf opam cmake
33
Download ada from https://www.adacore.com/download
34

    
35

    
36
Then
37
opam install ocamlfind ocamlgraph cmdliner fmt logs dune num yojson 
38

    
39

    
40
For the ADA backend:
41
- GNAT 2018 community edition on https://www.adacore.com/download
42
- gprbuild shall be in your path
43

    
44
# Build
45
```
46
> autoconf
47
> ./configure
48
> make
49
> make install
50
```
51

    
52
# Usage
53
```
54
> ./bin/lustrec -help
55
```
56

    
57
## Examples
58

    
59
In a modular setting:
60
`lustrec <filename.lus>`
61
will generate filename.c and filename.h
62

    
63
With a main node:
64
`lustrec -node <main_node> <filename.lus>`
65
will generate the same two files,
66
but also filename_main.c that contains a main function
67
and filename_alloc.h that contains the node allocation macros 
68

    
69
With a main node, with a static memory allocation scheme:
70
`lustrec -node <main_node> -dynamic <filename.lus>`
71
same as above, but main function will dynamically allocate node memory
72

    
73
To compile it:
74
```
75
gcc -Iinclude filename.c
76
gcc -Iinclude filename_main.c
77
```
78
where include links to the include folder
79

    
80
To run it with the generated main function:
81
- compile the io_frontend.o
82
```
83
gcc -c include/io_frontend.c
84
gcc -Iinclude -o target_name io_frontend.o filename.o filename_main.o
85
./target_name
86
``` 
87

    
88
To analyze it with frama-c
89
`frama-c -cpp-extra-args='-Iinclude'  filename.c`
90

    
91
# Contributors 
92

    
93
# Developer documentation
94

    
95
```
96
dune build @doc-private
97
```
98
The documentation is generated to `_build/default/_doc/_html/lustrec@XXXXXXXX/`
99

    
100
You can find non-code specific documentation in the `/doc` folder.
101

    
102
# People
103
* Pierre-Loic Garoche (ONERA)
104
* Xavier Thirioux (IRIT)
105
* Temesghen Kahsai (NASA Ames / CMU)
(7-7/11)