Project

General

Profile

Statistics
| Branch: | Tag: | Revision:
Name Size Revision Age Author Comment
  data-test 5c0d6e4e almost 6 years Christophe Garion json-parser: more tests with single variables
  doc 73ccaf2f almost 5 years Pierre-Loïc Garoche Merge branch 'cocospec' of https://cavale.ensee...
  include 0406ab94 over 2 years Lélio Brun implement optimization on spec: IT WORKS
  share 57c96fb7 over 2 years Lélio Brun setup tests for dune
  src 0406ab94 over 2 years Lélio Brun implement optimization on spec: IT WORKS
.gitignore 118 Bytes 719ae9fd over 2 years Lélio Brun migration draft on dune
.gitlab-ci.yml 13.5 KB 9d693675 over 2 years Lélio Brun the generation of ACSL from machine code reveal...
.gitmodules 86 Bytes 57c96fb7 over 2 years Lélio Brun setup tests for dune
.ocamlformat 121 Bytes 27502d69 over 2 years Lélio Brun add memory instances to footprint lemmas
AUTHORS 244 Bytes ec8fc65e almost 5 years Pierre-Loïc Garoche configure.ac tuning
INSTALL 290 Bytes 75a7b65b over 4 years Garoche install notes
LICENSE-LGPL.txt 25.8 KB 22fe1c93 almost 10 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler git-sv...
Makefile-lustresf.in 142 Bytes 3b4b7a2e almost 6 years Christophe Garion [lustresf] lustresf targets are optional in Mak...
Makefile.in 3.63 KB fb716d2c almost 5 years Pierre-Loïc Garoche Some autoconf update
README.lustrec 991 Bytes 7bfb18df over 8 years Xavier Thirioux updated version of README.lustrec about how to ...
README.md 1.04 KB 719ae9fd over 2 years Lélio Brun migration draft on dune
ReleaseProcess.txt 1.68 KB dd74ca16 almost 7 years Frederic Boniol Document release process
TODO.org 11.1 KB f4cba4b8 over 4 years Pierre-Loïc Garoche Some progress on compiling cocospec contract. C...
configure.ac 10.3 KB f0195e96 over 3 years Pierre-Loïc Garoche - Primitive Tiny backend - Renamed Mpfr to lust...
dune 1.27 KB ca7ff3f7 over 2 years Lélio Brun reformatting
dune-project 1.26 KB d0f26f04 over 2 years Lélio Brun corrections for stateless nodes
lustrec.opam 1.29 KB 97d4e95e over 2 years Lélio Brun add gmp dep
tests 0 Bytes 57c96fb7 over 2 years Lélio Brun setup tests for dune

Latest revisions

# Date Author Comment
0406ab94 06/18/2021 06:08 PM Lélio Brun

implement optimization on spec: IT WORKS

27502d69 06/18/2021 12:35 PM Lélio Brun

add memory instances to footprint lemmas

d0f26f04 06/17/2021 07:00 PM Lélio Brun

corrections for stateless nodes

ca7ff3f7 06/17/2021 11:33 AM Lélio Brun

reformatting

3ee26303 06/17/2021 10:19 AM Lélio Brun

conditionnally print spec in machine code logs

aaa8e454 06/16/2021 06:44 PM Lélio Brun

it works

1daf7bf0 06/16/2021 03:20 PM Lélio Brun

systematically add dependencies to clock variables in rhs

a91680fc 06/16/2021 01:24 PM Lélio Brun

Bug fix with constant inlining variable removal in machine code

c4780a6a 06/15/2021 05:34 PM Lélio Brun

work on new reset functions generation

6d1693b9 06/14/2021 07:06 PM Lélio Brun

work on spec generation almost done

View all revisions | View revisions

Also available in: Atom