Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec @ a56f563e

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

Latest revisions

# Date Author Comment
a56f563e 10/13/2021 06:42 PM Lélio Brun

more compact assign clauses for state variables, and remove useless memory pack predicates and assertions
0da3f528 10/07/2021 06:34 PM Lélio Brun

remove tests with include directives
7cb1f579 10/07/2021 06:33 PM Lélio Brun

reintroduce existential for variables that may appear free when performing substitution
hopefully those are less problematic since they actually exists in the program as variables
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

View all revisions | View revisions

Also available in: Atom