Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec @ 4174a469

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