Project

General

Profile

Statistics
| Branch: | Tag: | Revision:
Name Size Revision Age Author Comment
  backends 93d16170 almost 10 years Guillaume Davy Correct a bug in ensures stack generation relat...
Print.ml 2.69 KB 0cbf0839 almost 11 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
Print.mli 5.31 KB 0cbf0839 almost 11 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
access.ml 3.9 KB 0038002e about 10 years Pierre-Loïc Garoche Prepared first stage of code reorg: 1. moved ty...
basic_library.ml 7.28 KB e3945827 almost 10 years Guillaume Davy Push current status of proof backend
causality.ml 19 KB dae9db56 about 10 years Pierre-Loïc Garoche Version quasi fonctionnelle de la generation de...
clock_calculus.ml 30.2 KB 0038002e about 10 years Pierre-Loïc Garoche Prepared first stage of code reorg: 1. moved ty...
clock_predef.ml 1.77 KB 0cbf0839 almost 11 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
clocks.ml 19.3 KB 97498b53 over 10 years Xavier Thirioux still computing disjoint clock information (for...
com_protocol.ml 6.41 KB 0cbf0839 almost 11 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
corelang.ml 24.9 KB dae9db56 about 10 years Pierre-Loïc Garoche Version quasi fonctionnelle de la generation de...
corelang.mli 8.35 KB dae9db56 about 10 years Pierre-Loïc Garoche Version quasi fonctionnelle de la generation de...
deadline_calculus.ml 5.96 KB 0cbf0839 almost 11 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
deadlines.ml 2.58 KB 0cbf0839 almost 11 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
delay.ml 3.3 KB 0cbf0839 almost 11 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
delay_predef.ml 1.55 KB 0cbf0839 almost 11 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
dimension.ml 10.8 KB 6b4d172f over 10 years Xavier Thirioux - refactorization of typing code (simpler subty...
env.ml 1.95 KB aa223e69 over 10 years Xavier Thirioux more steps towards struct types... Cette ligne,...
expand.ml 11.1 KB 0cbf0839 almost 11 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
horn_backend.ml 22.8 KB 36454535 about 10 years Pierre-Loïc Garoche Merged horn_traces branch
init_calculus.ml 11.5 KB 0cbf0839 almost 11 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
init_predef.ml 2.62 KB 0cbf0839 almost 11 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
inliner.ml 11.9 KB e3945827 almost 10 years Guillaume Davy Push current status of proof backend
java_backend.ml 14.6 KB 0cbf0839 almost 11 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
lexerLustreSpec.mll 3.44 KB 0038002e about 10 years Pierre-Loïc Garoche Prepared first stage of code reorg: 1. moved ty...
lexer_lustre.mll 5.26 KB 45c0d258 over 10 years Pierre-Loïc Garoche Solved bug: - loading lusi - loading lib in lus...
lexer_prelude.mll 3.54 KB 0cbf0839 almost 11 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
liveness.ml 9.65 KB 1837ce98 about 10 years Xavier Thirioux added some infrastructure to ease optimization ...
location.ml 2.9 KB 45c0d258 over 10 years Pierre-Loïc Garoche Solved bug: - loading lusi - loading lib in lus...
log.ml 1.29 KB c00d0b42 over 10 years Pierre-Loïc Garoche Changed the load of lusi files: imported nodes ...
lustreSpec.ml 4.71 KB 36454535 about 10 years Pierre-Loïc Garoche Merged horn_traces branch
machine_code.ml 22.7 KB e3945827 almost 10 years Guillaume Davy Push current status of proof backend
main_lustre_compiler.ml 14.3 KB bd09b789 almost 10 years Guillaume Davy add coq support
normalization.ml 20.7 KB e3945827 almost 10 years Guillaume Davy Push current status of proof backend
optimize_machine.ml 3.71 KB 1837ce98 about 10 years Xavier Thirioux added some infrastructure to ease optimization ...
optimize_prog.ml 3.49 KB 0038002e about 10 years Pierre-Loïc Garoche Prepared first stage of code reorg: 1. moved ty...
options.ml 4.71 KB 690cde69 almost 10 years Pierre-Loïc Garoche Added an option for let vs exists axiomatization
parse.ml 1.91 KB 2ea1e4a6 over 10 years Xavier Thirioux corrected bugs in clock generalization that pro...
parserLustreSpec.mly 7.28 KB 0038002e about 10 years Pierre-Loïc Garoche Prepared first stage of code reorg: 1. moved ty...
parser_lustre.mly 16.6 KB 0038002e about 10 years Pierre-Loïc Garoche Prepared first stage of code reorg: 1. moved ty...
precedence_functions.ml 2.92 KB 0cbf0839 almost 11 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
printers.ml 18.7 KB 36454535 about 10 years Pierre-Loïc Garoche Merged horn_traces branch
scheduling.ml 8.33 KB dae9db56 about 10 years Pierre-Loïc Garoche Version quasi fonctionnelle de la generation de...
sortProg.ml 1.31 KB 0038002e about 10 years Pierre-Loïc Garoche Prepared first stage of code reorg: 1. moved ty...
splitting.ml 4.06 KB dae9db56 about 10 years Pierre-Loïc Garoche Version quasi fonctionnelle de la generation de...
stateless.ml 3.2 KB 5538b7ac over 10 years Xavier Thirioux Added declaration/definition of stateless/state...
type_predef.ml 2.85 KB 6b4d172f over 10 years Xavier Thirioux - refactorization of typing code (simpler subty...
types.ml 9.85 KB d96d54ac about 10 years Xavier Thirioux added construction of a fanin table for local v...
typing.ml 28.7 KB 36454535 about 10 years Pierre-Loïc Garoche Merged horn_traces branch
utils.ml 9.07 KB 1837ce98 about 10 years Xavier Thirioux added some infrastructure to ease optimization ...

Latest revisions

# Date Author Comment
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

690cde69 11/13/2014 10:59 AM Pierre-Loïc Garoche

Added an option for let vs exists axiomatization

65de0e13 11/06/2014 02:54 PM Guillaume Davy

ALT2 proved by framaC without human interaction

bff13707 11/05/2014 05:15 PM Guillaume Davy

ALT_2 working with modification made by hand

a93ebdab 11/05/2014 10:46 AM Guillaume Davy

Correct bug option exists

23c510d0 11/05/2014 09:29 AM Guillaume Davy

Update on c backend proof

0ba542d7 10/29/2014 11:55 PM Guillaume Davy

Bugfixes and coq proof generation for lemma inv_inv

faa5c6db 10/23/2014 01:00 PM Pierre-Loïc Garoche

solved the bug of multiple definition of assert exists ...

bd09b789 10/23/2014 12:59 PM Guillaume Davy

add coq support

View revisions

Also available in: Atom