lustrec/src @ 7f03f62d
Name | Size | Revision | Age | Author | Comment |
---|---|---|---|---|---|
backends | 7f03f62d | over 3 years | Lélio Brun | first version that is parsed correctly by Frama-C | |
checks | 15c3e4e7 | over 3 years | Lélio Brun | generic ACSL spec generation | |
features | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings | |
parsers | 2756319f | over 3 years | Lélio Brun | messages d'erreurs terminés | |
plugins | 90cc3b8e | over 3 years | Lélio Brun | some rewriting in C backend pretty-printer | |
tools | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings | |
utils | a2327c71 | over 3 years | Lélio Brun | start to write error messages | |
Makefile-lustresf.in | 758 Bytes | 3b4b7a2e | over 6 years | Christophe Garion | [lustresf] lustresf targets are optional in Mak... |
Makefile.in | 1.58 KB | 325f07c0 | over 5 years | Christophe Garion | doc: use SVG format instead of PNG for dependen... |
_tags.in | 2.04 KB | b43b8eb5 | over 3 years | Pierre-Loic Garoche | add thread dependency required by z3 lib |
annotations.ml | 1.16 KB | 8446bf03 | over 6 years | Pierre-Loïc Garoche | - Makefile: solved dependency problem when comp... |
arrow.ml | 837 Bytes | 719ae9fd | over 3 years | Lélio Brun | migration draft on dune |
arrow.mli | 110 Bytes | 719ae9fd | over 3 years | Lélio Brun | migration draft on dune |
automata.ml | 14.8 KB | 57c96fb7 | over 3 years | Lélio Brun | setup tests for dune |
basic_library.ml | 11.2 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
causality.ml | 25.5 KB | 90e83deb | over 3 years | Lélio Brun | prepare for the modern error handling of Menhir |
clock_calculus.ml | 27 KB | 90e83deb | over 3 years | Lélio Brun | prepare for the modern error handling of Menhir |
clock_predef.ml | 1.76 KB | ec433d69 | over 9 years | Xavier Thirioux | Major revision due to severe limitations and bu... |
clocks.ml | 14 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
compiler_common.ml | 14.5 KB | a2327c71 | over 3 years | Lélio Brun | start to write error messages |
compiler_stages.ml | 12.8 KB | 1df55e58 | over 3 years | Lélio Brun | minor rewriting |
corelang.ml | 48 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
corelang.mli | 8.05 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
delay.ml | 2.97 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
delay_predef.ml | 1.28 KB | ea8f51ae | over 6 years | Pierre-Loïc Garoche | Basic library printers moved into backend speci... |
dune | 3.38 KB | 90e83deb | over 3 years | Lélio Brun | prepare for the modern error handling of Menhir |
error.ml | 1.82 KB | 04a188ec | almost 5 years | Pierre-Loïc Garoche | - Refactored Error exception and messages - Bug... |
expand.ml | 10.8 KB | ea8f51ae | over 6 years | Pierre-Loïc Garoche | Basic library printers moved into backend speci... |
global.ml | 651 Bytes | 04a188ec | almost 5 years | Pierre-Loïc Garoche | - Refactored Error exception and messages - Bug... |
init_predef.ml | 2.29 KB | ea8f51ae | over 6 years | Pierre-Loïc Garoche | Basic library printers moved into backend speci... |
inliner.ml | 20 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
log.ml | 1 KB | 15c3e4e7 | over 3 years | Lélio Brun | generic ACSL spec generation |
lusic.ml | 3.63 KB | c226a3ba | over 3 years | Lélio Brun | start generating ACSL spec |
lustre_types.ml | 7.08 KB | 04a188ec | almost 5 years | Pierre-Loïc Garoche | - Refactored Error exception and messages - Bug... |
lustre_utils.ml | 3.99 KB | b8dfc744 | about 5 years | Pierre-Loïc Garoche | valid _verif node for seal-export lustre |
lustrec.odocl | 1.05 KB | aa85bd44 | over 5 years | Guillaume DAVY | Doc: update rule and remove old module in odocl |
machine_code.ml | 16.6 KB | 1df55e58 | over 3 years | Lélio Brun | minor rewriting |
machine_code.mli | 135 Bytes | f4cba4b8 | over 5 years | Pierre-Loïc Garoche | Some progress on compiling cocospec contract. C... |
machine_code_common.ml | 11.6 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
machine_code_common.mli | 1.91 KB | f0195e96 | over 4 years | Pierre-Loïc Garoche | - Primitive Tiny backend - Renamed Mpfr to lust... |
machine_code_types.ml | 1.72 KB | 1fd3d002 | over 5 years | Pierre-Loïc Garoche | Cocospec: parsing, normalizing and processing m... |
main_lustre_compiler.ml | 4.94 KB | 90e83deb | over 3 years | Lélio Brun | prepare for the modern error handling of Menhir |
main_lustre_testgen.ml | 7.19 KB | 57c96fb7 | over 3 years | Lélio Brun | setup tests for dune |
main_lustre_verifier.ml | 5.45 KB | 90e83deb | over 3 years | Lélio Brun | prepare for the modern error handling of Menhir |
mmap.ml | 10.7 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
modules.ml | 12.1 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
modules.mli | 867 Bytes | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
mutation.ml | 26.8 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
normalization.ml | 32.8 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
normalization.mli | 319 Bytes | 95944ba1 | almost 6 years | Pierre-Loïc Garoche | Cleaning up stuff in normalization. Mainly repl... |
optimize_machine.ml | 31.6 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
optimize_prog.ml | 4.56 KB | e47138b8 | almost 5 years | Pierre-Loïc Garoche | reactivating the unfolding of constants |
options.ml | 2.11 KB | a0c92fa8 | over 4 years | Pierre-Loïc Garoche | printing nodes + more progress on seal export |
options_management.ml | 8.58 KB | 90cc3b8e | over 3 years | Lélio Brun | some rewriting in C backend pretty-printer |
pathConditions.ml | 11.7 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
printers.ml | 22.8 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
real.ml | 1.44 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
real.mli | 619 Bytes | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
scheduling.ml | 10.3 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
scheduling_type.ml | 557 Bytes | a703ed0c | almost 6 years | Pierre-Loïc Garoche | Preprocess the selected node in seaL BACKEND: f... |
sortProg.ml | 2.23 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
spec.ml | 524 Bytes | 8446bf03 | over 6 years | Pierre-Loïc Garoche | - Makefile: solved dependency problem when comp... |
splitting.ml | 3.16 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
type_predef.ml | 3.2 KB | ea8f51ae | over 6 years | Pierre-Loïc Garoche | Basic library printers moved into backend speci... |
types.ml | 16.6 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
typing.ml | 39.5 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
verifierList.ml | 176 Bytes | 719ae9fd | over 3 years | Lélio Brun | migration draft on dune |
verifierType.ml | 504 Bytes | 7a4fd94d | about 5 years | Pierre-Loïc Garoche | Output folder for seal-extract |
verifiers.ml | 1.26 KB | ca7e8027 | over 3 years | Lélio Brun | fix almost all warnings |
version.ml | 183 Bytes | ac6ce5a1 | over 3 years | Lélio Brun | disable tests in gitlab CI |
Latest revisions
Also available in: Atom