Project

General

Profile

Statistics
| Branch: | Tag: | Revision:
Name Size Revision Age Author Comment
  data-test 5c0d6e4e over 6 years Christophe Garion json-parser: more tests with single variables
  doc 73ccaf2f over 5 years Pierre-Loïc Garoche Merge branch 'cocospec' of https://cavale.ensee...
  docker d10d0cd9 over 2 years Lélio Brun Docker files
  include d978c46e almost 3 years Lélio Brun start instrumenting the main C function
  offline_tests d119be37 over 2 years Lélio Brun fix test script
  share 57c96fb7 over 3 years Lélio Brun setup tests for dune
  src 3d1f9d9f over 2 years Lélio Brun more agressive optim propagation in spec in ord...
  unused d29fbec5 over 2 years Lélio Brun working version for stateful contracts
.gitignore 118 Bytes 719ae9fd over 3 years Lélio Brun migration draft on dune
.gitlab-ci.yml 13.5 KB 9d693675 about 3 years Lélio Brun the generation of ACSL from machine code reveal...
.gitmodules 86 Bytes 57c96fb7 over 3 years Lélio Brun setup tests for dune
.mailmap 1.37 KB 1bb31f65 almost 3 years Lélio Brun a mailmap to clarify logs
.ocamlformat 141 Bytes d29fbec5 over 2 years Lélio Brun working version for stateful contracts
AUTHORS 244 Bytes ec8fc65e over 5 years Pierre-Loïc Garoche configure.ac tuning
INSTALL 290 Bytes 75a7b65b about 5 years Garoche install notes
LICENSE-LGPL.txt 25.8 KB 22fe1c93 over 10 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler git-sv...
Makefile-lustresf.in 142 Bytes 3b4b7a2e over 6 years Christophe Garion [lustresf] lustresf targets are optional in Mak...
Makefile.in 3.63 KB fb716d2c over 5 years Pierre-Loïc Garoche Some autoconf update
README.lustrec 991 Bytes 7bfb18df about 9 years Xavier Thirioux updated version of README.lustrec about how to ...
README.md 1.04 KB 719ae9fd over 3 years Lélio Brun migration draft on dune
ReleaseProcess.txt 1.68 KB dd74ca16 over 7 years Frederic Boniol Document release process
TODO.org 11.1 KB f4cba4b8 over 5 years Pierre-Loïc Garoche Some progress on compiling cocospec contract. C...
configure.ac 10.3 KB f0195e96 over 4 years Pierre-Loïc Garoche - Primitive Tiny backend - Renamed Mpfr to lust...
dune 1.34 KB 10131419 over 2 years Lélio Brun add offline tests and fix a bug in generated sp...
dune-project 1.26 KB 70710795 almost 3 years Lélio Brun first draft with translated cocospec
lustrec.opam 1.38 KB dccec723 over 2 years Lélio Brun a version that almost work for the k-inuctive t...
rundocker.sh 376 Bytes d10d0cd9 over 2 years Lélio Brun Docker files
tests 0 Bytes 57c96fb7 over 3 years Lélio Brun setup tests for dune

Latest revisions

# Date Author Comment
3d1f9d9f 10/07/2021 01:27 PM Lélio Brun

more agressive optim propagation in spec in order to remove unecessarry existential variables that were eliminated (helps the solvers)

d119be37 10/07/2021 10:30 AM Lélio Brun

fix test script

74ebe1f9 10/06/2021 06:32 PM Lélio Brun

fix bug in handling state variables in nested expressions

4240dfcb 10/06/2021 06:04 PM Lélio Brun

add basic support to protect against some ACSL keywords

e164da10 10/06/2021 05:12 PM Lélio Brun

fix live variable calculation for spec: take variables occuring in clocks into account

fb6e2cfd 10/06/2021 12:52 PM Lélio Brun

print (*mem) instead of *mem to avoid ambiguities with accesses

e77a0fa5 10/06/2021 11:25 AM Lélio Brun

fix handling of state variables in spec expressions

81d69074 10/06/2021 10:18 AM Lélio Brun

fix bug where singleton tuples were generated

569e560f 10/05/2021 01:59 PM Lélio Brun

test everything

9c227bad 10/05/2021 01:55 PM Lélio Brun

fix offline tests

View all revisions | View revisions

Also available in: Atom