Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec @ 6a93d814

Name Size Revision Age Author Comment
  doc fdeaac38 almost 8 years Pierre-Loïc Garoche Lustre interfaces: lusi files are generated and...
  example_twocounters 2bdbbe54 almost 7 years Guillaume Davy Add tests from fmcad with k annotation to new_b...
  include f044d0b0 over 7 years Pierre-Loïc Garoche Convertion operators
  optim 6a93d814 over 6 years Xavier Thirioux added a directory optim/ dedicated to experimen...
  scripts 6a93d814 over 6 years Xavier Thirioux added a directory optim/ dedicated to experimen...
  src 4174a469 almost 7 years Guillaume Davy Correct some problem related to new bool encoding
  tcm_benchmarks 4174a469 almost 7 years Guillaume Davy Correct some problem related to new bool encoding
  test 36454535 about 7 years Pierre-Loïc Garoche Merged horn_traces branch
  tests 6a93d814 over 6 years Xavier Thirioux added a directory optim/ dedicated to experimen...
AUTHORS 61 Bytes c00d0b42 over 7 years Pierre-Loïc Garoche Changed the load of lusi files: imported nodes ...
LICENSE-LGPL.txt 25.8 KB 0cbf0839 almost 8 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
Makefile 702 Bytes 9aaee7f9 about 7 years Xavier Thirioux added warnings for useless variables (at verbos...
README.lustrec 802 Bytes 0cbf0839 almost 8 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
TODO.org 1.13 KB 0cbf0839 almost 8 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
_oasis 600 Bytes c00d0b42 over 7 years Pierre-Loïc Garoche Changed the load of lusi files: imported nodes ...
_tags 740 Bytes f6fa97f9 over 7 years Xavier Thirioux clean handling of undefined node application
configure 364 Bytes 9aaee7f9 about 7 years Xavier Thirioux added warnings for useless variables (at verbos...
myocamlbuild.ml 13.7 KB 9aaee7f9 about 7 years Xavier Thirioux added warnings for useless variables (at verbos...
setup.ml 154 KB 9aaee7f9 about 7 years Xavier Thirioux added warnings for useless variables (at verbos...
svn_version.sh 558 Bytes c6acbdaa over 7 years Xavier Thirioux answer to #feature 50: - arrows are now factor...
svnignore 103 Bytes 0cbf0839 almost 8 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler

Latest revisions

# Date Author Comment
6a93d814 04/09/2015 01:24 PM Xavier Thirioux

added a directory optim/ dedicated to experiments about injecting/proving ACSL spec into optimized programs.

cc9e1901 12/26/2014 10:18 PM Pierre-Loïc Garoche

Added results of the first analysis

08bbd713 12/23/2014 08:03 AM Pierre-Loïc Garoche

uploaded scripts

e5d5c450 12/23/2014 07:25 AM Pierre-Loïc Garoche

Mem limit + issues with log and pdflatex log

13b22bd5 12/22/2014 10:21 PM Pierre-Loïc Garoche

Solved some bugs in the scripts: invalid path for report style files and blocking pdflatex

0ec278d2 12/22/2014 04:36 PM Pierre-Loïc Garoche

cleaning

a06b22fd 12/22/2014 04:28 PM Pierre-Loïc Garoche

Moved scripts here

94a4b867 12/22/2014 04:28 PM Pierre-Loïc Garoche

worklist for parallel

82398d1d 12/22/2014 02:28 PM Pierre-Loïc Garoche

Frama-C WP report templates

2b7729d4 12/22/2014 02:27 PM Pierre-Loïc Garoche

On going work. Generating report focusing on proved vs unproved part

View all revisions | View revisions

Also available in: Atom