Project

General

Profile

« Previous | Next » 

Revision dbc69edc

Added by Corentin Lauverjat over 1 year ago

  • ID dbc69edc9425c1b5f291583739fb0d7c3401a8c5
  • Parent 8c36178f

Passage à dune

View differences:

README.md
1
Current status : [![Build Status](https://travis-ci.org/coco-team/lustrec.svg?branch=master)](https://travis-ci.org/coco-team/lustrec)
1 2

  
2
Current Status:    [![Build Status](https://travis-ci.org/coco-team/lustrec.svg?branch=master)](https://travis-ci.org/coco-team/lustrec)
3

  
4
[![Stories in Ready](https://badge.waffle.io/coco-team/lustrec.png?label=ready&title=Ready)](https://waffle.io/coco-team/lustrec)
5
[![Throughput Graph](https://graphs.waffle.io/coco-team/lustrec/throughput.svg)](https://waffle.io/coco-team/lustrec/metrics/throughput)
6

  
7
# LustreC
3
# About LustreC
8 4

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

  
11 7
# Dependencies
12
On a fresh ubuntu/debian-like install
8

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

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

  
21 44
# Build
22 45
```
23 46
> autoconf
24 47
> ./configure
25 48
> make
49
> make install
26 50
```
27 51

  
28 52
# Usage
......
30 54
> ./bin/lustrec -help
31 55
```
32 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

  
33 102
# People
34 103
* Pierre-Loic Garoche (ONERA)
35 104
* Xavier Thirioux (IRIT)

Also available in: Unified diff