Project

General

Profile

Statistics
| Branch: | Tag: | Revision:
Name Size Revision Age Author Comment
  backends 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
  checks 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
  features ca7e8027 11 months Lélio Brun fix almost all warnings
  parsers 2756319f 10 months Lélio Brun messages d'erreurs terminés
  plugins 90cc3b8e 11 months Lélio Brun some rewriting in C backend pretty-printer
  tools ca7e8027 11 months Lélio Brun fix almost all warnings
  utils 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
Makefile-lustresf.in 758 Bytes 3b4b7a2e about 4 years Christophe Garion [lustresf] lustresf targets are optional in Mak...
Makefile.in 1.58 KB 325f07c0 almost 3 years Christophe Garion doc: use SVG format instead of PNG for dependen...
_tags.in 2.04 KB b43b8eb5 12 months Pierre-Loic Garoche add thread dependency required by z3 lib
annotations.ml 1.16 KB 8446bf03 almost 4 years Pierre-Loïc Garoche - Makefile: solved dependency problem when comp...
arrow.ml 837 Bytes 719ae9fd 12 months Lélio Brun migration draft on dune
arrow.mli 110 Bytes 719ae9fd 12 months Lélio Brun migration draft on dune
automata.ml 14.8 KB 57c96fb7 11 months Lélio Brun setup tests for dune
basic_library.ml 11.2 KB ca7e8027 11 months Lélio Brun fix almost all warnings
causality.ml 25.5 KB 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
clock_calculus.ml 27.1 KB 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
clock_predef.ml 1.76 KB ec433d69 almost 7 years Xavier Thirioux Major revision due to severe limitations and bu...
clocks.ml 14 KB ca7e8027 11 months Lélio Brun fix almost all warnings
compiler_common.ml 14.6 KB 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
compiler_stages.ml 13.1 KB 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
corelang.ml 48 KB ca7e8027 11 months Lélio Brun fix almost all warnings
corelang.mli 8.05 KB ca7e8027 11 months Lélio Brun fix almost all warnings
delay.ml 2.97 KB ca7e8027 11 months Lélio Brun fix almost all warnings
delay_predef.ml 1.28 KB ea8f51ae almost 4 years Pierre-Loïc Garoche Basic library printers moved into backend speci...
dune 3.38 KB 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
error.ml 1.82 KB 04a188ec about 2 years Pierre-Loïc Garoche - Refactored Error exception and messages - Bug...
expand.ml 10.8 KB ea8f51ae almost 4 years Pierre-Loïc Garoche Basic library printers moved into backend speci...
global.ml 651 Bytes 04a188ec about 2 years Pierre-Loïc Garoche - Refactored Error exception and messages - Bug...
init_predef.ml 2.29 KB ea8f51ae almost 4 years Pierre-Loïc Garoche Basic library printers moved into backend speci...
inliner.ml 20 KB ca7e8027 11 months Lélio Brun fix almost all warnings
log.ml 1020 Bytes 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
lusic.ml 3.53 KB efcc8d7f 9 months Lélio Brun move arrow spec in its own header
lustre_types.ml 7.08 KB 04a188ec about 2 years Pierre-Loïc Garoche - Refactored Error exception and messages - Bug...
lustre_utils.ml 3.99 KB b8dfc744 over 2 years Pierre-Loïc Garoche valid _verif node for seal-export lustre
lustrec.odocl 1.05 KB aa85bd44 almost 3 years Guillaume DAVY Doc: update rule and remove old module in odocl
machine_code.ml 14.8 KB 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
machine_code.mli 135 Bytes f4cba4b8 almost 3 years Pierre-Loïc Garoche Some progress on compiling cocospec contract. C...
machine_code_common.ml 11.9 KB 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
machine_code_common.mli 1.98 KB 9d693675 9 months Lélio Brun the generation of ACSL from machine code reveal...
machine_code_types.ml 1.82 KB 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
main_lustre_compiler.ml 4.96 KB 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
main_lustre_testgen.ml 7.19 KB 57c96fb7 11 months Lélio Brun setup tests for dune
main_lustre_verifier.ml 5.45 KB 90e83deb 10 months Lélio Brun prepare for the modern error handling of Menhir
mmap.ml 10.7 KB ca7e8027 11 months Lélio Brun fix almost all warnings
modules.ml 12.1 KB ca7e8027 11 months Lélio Brun fix almost all warnings
modules.mli 867 Bytes ca7e8027 11 months Lélio Brun fix almost all warnings
mutation.ml 26.8 KB ca7e8027 11 months Lélio Brun fix almost all warnings
normalization.ml 32.8 KB ca7e8027 11 months Lélio Brun fix almost all warnings
normalization.mli 319 Bytes 95944ba1 about 3 years Pierre-Loïc Garoche Cleaning up stuff in normalization. Mainly repl...
optimize_machine.ml 32 KB 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
optimize_prog.ml 4.56 KB e47138b8 about 2 years Pierre-Loïc Garoche reactivating the unfolding of constants
options.ml 2.11 KB a0c92fa8 almost 2 years Pierre-Loïc Garoche printing nodes + more progress on seal export
options_management.ml 8.58 KB 90cc3b8e 11 months Lélio Brun some rewriting in C backend pretty-printer
pathConditions.ml 11.7 KB ca7e8027 11 months Lélio Brun fix almost all warnings
printers.ml 22.7 KB 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
real.ml 1.44 KB ca7e8027 11 months Lélio Brun fix almost all warnings
real.mli 619 Bytes ca7e8027 11 months Lélio Brun fix almost all warnings
scheduling.ml 10.5 KB 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
scheduling_type.ml 557 Bytes a703ed0c about 3 years Pierre-Loïc Garoche Preprocess the selected node in seaL BACKEND: f...
sortProg.ml 2.25 KB 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
spec.ml 524 Bytes 8446bf03 almost 4 years Pierre-Loïc Garoche - Makefile: solved dependency problem when comp...
splitting.ml 3.16 KB ca7e8027 11 months Lélio Brun fix almost all warnings
type_predef.ml 3.2 KB ea8f51ae almost 4 years Pierre-Loïc Garoche Basic library printers moved into backend speci...
types.ml 16.6 KB ca7e8027 11 months Lélio Brun fix almost all warnings
typing.ml 39.6 KB 7ee5f69e 9 months Lélio Brun corrections on loggers + spec in AST
verifierList.ml 176 Bytes 719ae9fd 12 months Lélio Brun migration draft on dune
verifierType.ml 504 Bytes 7a4fd94d over 2 years Pierre-Loïc Garoche Output folder for seal-extract
verifiers.ml 1.26 KB ca7e8027 11 months Lélio Brun fix almost all warnings
version.ml 183 Bytes ac6ce5a1 11 months Lélio Brun disable tests in gitlab CI

Latest revisions

# Date Author Comment
7ee5f69e 05/04/2021 10:20 AM Lélio Brun

corrections on loggers + spec in AST

dfce5630 04/26/2021 05:12 PM Lélio Brun

patch de Xavier pour réparer -O 3

9d693675 04/22/2021 03:06 PM Lélio Brun

the generation of ACSL from machine code reveal too fragile as it occurs after several transformations (eg. fusion)

efcc8d7f 04/21/2021 05:15 PM Lélio Brun

move arrow spec in its own header

186e1aef 04/21/2021 01:52 PM Lélio Brun

working proto

8d2d6fa0 04/20/2021 06:51 PM Lélio Brun

Almost works!

7f03f62d 04/16/2021 11:33 AM Lélio Brun

first version that is parsed correctly by Frama-C

4b596770 04/12/2021 05:48 PM Lélio Brun

first draft: to be tested with frama-c

2756319f 03/29/2021 11:12 AM Lélio Brun

messages d'erreurs terminés

e78eb9f5 03/25/2021 06:23 PM Lélio Brun

more error messages

View revisions

Also available in: Atom