Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec @ 4174a469

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

Latest revisions

# Date Author Comment
4174a469 12/19/2014 10:50 PM Guillaume Davy

Correct some problem related to new bool encoding
105b3645 12/19/2014 10:50 PM Guillaume Davy

Delete tests files that have no k
d3a3e7e9 12/18/2014 10:07 PM Pierre-Loïc Garoche

SMT2 file generated by frama-c/why3/z3-edit - it is the second base case of kinduction of ALT3. And it is not provable.
995bfad5 12/18/2014 02:45 PM Guillaume Davy

Add the script used to add k annotation to tests.
2bdbbe54 12/18/2014 02:40 PM Guillaume Davy

Add tests from fmcad with k annotation to new_backend branch
e8b5876f 12/17/2014 09:11 PM Pierre-Loïc Garoche

modified version with pure k induction
af0ff493 12/16/2014 08:10 AM Pierre-Loïc Garoche

Removed unused predicate
5b12f571 12/16/2014 12:23 AM Pierre-Loïc Garoche

Example on possible encoding using the 5-inductive two counter example.
93d16170 11/15/2014 01:30 PM Guillaume Davy

Correct a bug in ensures stack generation related to existential
97602f7c 11/13/2014 11:48 AM Guillaume Davy

Correct bug when there is no precondition and change reprensentation
of boolean in ACSL

View all revisions | View revisions

Also available in: Atom