Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src @ 81229f63

Name Size Revision Age Author Comment
  backends 05f85b44 8 months Guillaume DAVY Ada: Start cleaning Ada to prepare for why beckend
  checks f4cba4b8 9 months Pierre-Loïc Garoche Some progress on compiling cocospec contract. C...
  features 95944ba1 about 1 year Pierre-Loïc Garoche Cleaning up stuff in normalization. Mainly repl...
  parsers 1fd3d002 9 months Pierre-Loïc Garoche Cocospec: parsing, normalizing and processing m...
  plugins e5d77428 7 months Pierre-Loïc Garoche Solved issue btw mpfr and conv functions (int_t...
  tools 81229f63 5 months Pierre-Loïc Garoche Seal-extract: first serious version. Guards are...
  utils f4cba4b8 9 months Pierre-Loïc Garoche Some progress on compiling cocospec contract. C...
.merlin 3 Bytes ae7d913d about 1 year Pierre-Loïc Garoche Merlin files
Makefile-lustresf.in 758 Bytes 3b4b7a2e about 2 years Christophe Garion [lustresf] lustresf targets are optional in Mak...
Makefile.in 1.58 KB 325f07c0 8 months Christophe Garion doc: use SVG format instead of PNG for dependen...
_tags.in 1.92 KB d5ec9f63 9 months Pierre-Loïc Garoche Minor modif on seal
annotations.ml 1.16 KB 8446bf03 over 1 year Pierre-Loïc Garoche - Makefile: solved dependency problem when comp...
arrow.ml 834 Bytes f4cba4b8 9 months Pierre-Loïc Garoche Some progress on compiling cocospec contract. C...
arrow.mli 102 Bytes 2863281f over 1 year Pierre-Loïc Garoche Further restructuring: - arrow.ml* to define ba...
automata.ml 14.8 KB f4cba4b8 9 months Pierre-Loïc Garoche Some progress on compiling cocospec contract. C...
basic_library.ml 6.57 KB ea8f51ae over 1 year Pierre-Loïc Garoche Basic library printers moved into backend speci...
causality.ml 25.5 KB 861f327f 9 months Pierre-Loïc Garoche Resolved sort order of nodes
clock_calculus.ml 27.1 KB 1fd3d002 9 months Pierre-Loïc Garoche Cocospec: parsing, normalizing and processing m...
clock_predef.ml 1.76 KB ec433d69 over 4 years Xavier Thirioux Major revision due to severe limitations and bu...
clocks.ml 13.9 KB 1fd3d002 9 months Pierre-Loïc Garoche Cocospec: parsing, normalizing and processing m...
compiler_common.ml 14.4 KB 4034b51c 9 months Pierre-Loïc Garoche more explanation in case of failure. Still dirty
compiler_stages.ml 12 KB 49d364b8 5 months Pierre-Loïc Garoche comestic changes, removing useless logs
corelang.ml 46.8 KB 81229f63 5 months Pierre-Loïc Garoche Seal-extract: first serious version. Guards are...
corelang.mli 8.12 KB 81229f63 5 months Pierre-Loïc Garoche Seal-extract: first serious version. Guards are...
delay.ml 2.97 KB ea8f51ae over 1 year Pierre-Loïc Garoche Basic library printers moved into backend speci...
delay_predef.ml 1.28 KB ea8f51ae over 1 year Pierre-Loïc Garoche Basic library printers moved into backend speci...
dimension.ml 10.9 KB 333e3a25 almost 2 years Pierre-Loïc Garoche [general] Refactor get_node_eqs to produce (eqs...
error.ml 1.77 KB f4cba4b8 9 months Pierre-Loïc Garoche Some progress on compiling cocospec contract. C...
expand.ml 10.8 KB ea8f51ae over 1 year Pierre-Loïc Garoche Basic library printers moved into backend speci...
global.ml 616 Bytes 49d364b8 5 months Pierre-Loïc Garoche comestic changes, removing useless logs
init_predef.ml 2.29 KB ea8f51ae over 1 year Pierre-Loïc Garoche Basic library printers moved into backend speci...
inliner.ml 20.1 KB f4cba4b8 9 months Pierre-Loïc Garoche Some progress on compiling cocospec contract. C...
location.ml 3.44 KB ea8f51ae over 1 year Pierre-Loïc Garoche Basic library printers moved into backend speci...
log.ml 1.01 KB 61df3cb9 9 months Pierre-Loïc Garoche Reformating plugin signatures. Better report ma...
lusic.ml 3.53 KB 19a1e66b about 1 year Pierre-Loïc Garoche Added include directive that directly inject a ...
lustre_types.ml 7.11 KB df94cd73 5 months Pierre-Loïc Garoche - More systematic translation for mutation - co...
lustrec.odocl 1.05 KB aa85bd44 8 months Guillaume DAVY Doc: update rule and remove old module in odocl
machine_code.ml 16.4 KB 1fd3d002 9 months Pierre-Loïc Garoche Cocospec: parsing, normalizing and processing m...
machine_code.mli 135 Bytes f4cba4b8 9 months Pierre-Loïc Garoche Some progress on compiling cocospec contract. C...
machine_code_common.ml 11.7 KB 867276c9 8 months Guillaume DAVY Machine_code: Make a correction in the arrow ma...
machine_code_common.mli 1.84 KB 70be4acf 9 months Pierre-Loïc Garoche Serious refactoring of scopes plug-in: - now pr...
machine_code_types.ml 1.72 KB 1fd3d002 9 months Pierre-Loïc Garoche Cocospec: parsing, normalizing and processing m...
main_lustre_compiler.ml 4.76 KB 61df3cb9 9 months Pierre-Loïc Garoche Reformating plugin signatures. Better report ma...
main_lustre_testgen.ml 6.97 KB 653b62e0 5 months Pierre-Loïc Garoche lustret: do not reload opened modules when gene...
main_lustre_verifier.ml 5.19 KB 6c3f2837 5 months Pierre-Loïc Garoche lustrev: removed the check of no dependencies
mmap.ml 10.7 KB 40d33d55 over 2 years Xavier Thirioux first version (doesn't even compile) of mutatio...
modules.ml 11.2 KB 3050ca8f 5 months Pierre-Loïc Garoche keep the open top declaration when loading a mo...
modules.mli 878 Bytes 5fccce23 about 1 year Pierre-Loïc Garoche - Dep type with a tuple has been replaced by a ...
mutation.ml 26.9 KB df94cd73 5 months Pierre-Loïc Garoche - More systematic translation for mutation - co...
normalization.ml 32.1 KB 1fd3d002 9 months Pierre-Loïc Garoche Cocospec: parsing, normalizing and processing m...
normalization.mli 319 Bytes 95944ba1 about 1 year Pierre-Loïc Garoche Cleaning up stuff in normalization. Mainly repl...
ocaml_utils.ml.in 31 Bytes c80e92d1 about 2 years Pierre-Loïc Garoche Solving a warning with ocaml 4.04 and uppercase...
optimize_machine.ml 26.3 KB 1fd3d002 9 months Pierre-Loïc Garoche Cocospec: parsing, normalizing and processing m...
optimize_prog.ml 4.43 KB d0b1ec56 about 5 years Xavier Thirioux - changed the basic optimization scheme (option...
options.ml 1.93 KB 3cd040e3 over 1 year Pierre-Loïc Garoche Issues with typing pp_basic_lib_fun
options_management.ml 8.42 KB 61df3cb9 9 months Pierre-Loïc Garoche Reformating plugin signatures. Better report ma...
pathConditions.ml 11.7 KB 2104c80a 5 months Pierre-Loïc Garoche Addressed a TODO in MCDC Pathconditions: simple...
pluginList.ml.in 77 Bytes ad4774b0 over 1 year Pierre-Loïc Garoche - Normalization parameters (alias and unfold_ar...
pluginType.ml 852 Bytes 61df3cb9 9 months Pierre-Loïc Garoche Reformating plugin signatures. Better report ma...
plugins.ml 1.72 KB 61df3cb9 9 months Pierre-Loïc Garoche Reformating plugin signatures. Better report ma...
printers.ml 19.3 KB 67ef9395 5 months Pierre-Loïc Garoche minor bugs solved in printer: guarantee vs guar...
scheduling.ml 9.52 KB f4cba4b8 9 months Pierre-Loïc Garoche Some progress on compiling cocospec contract. C...
scheduling_type.ml 557 Bytes a703ed0c about 1 year Pierre-Loïc Garoche Preprocess the selected node in seaL BACKEND: f...
sortProg.ml 2.24 KB 861f327f 9 months Pierre-Loïc Garoche Resolved sort order of nodes
spec.ml 524 Bytes 8446bf03 over 1 year Pierre-Loïc Garoche - Makefile: solved dependency problem when comp...
splitting.ml 3.18 KB 8446bf03 over 1 year Pierre-Loïc Garoche - Makefile: solved dependency problem when comp...
type_predef.ml 3.2 KB ea8f51ae over 1 year Pierre-Loïc Garoche Basic library printers moved into backend speci...
types.ml 16.5 KB ea8f51ae over 1 year Pierre-Loïc Garoche Basic library printers moved into backend speci...
typing.ml 39.6 KB 4034b51c 9 months Pierre-Loïc Garoche more explanation in case of failure. Still dirty
verifierList.ml.in 83 Bytes ad4774b0 over 1 year Pierre-Loïc Garoche - Normalization parameters (alias and unfold_ar...
verifierType.ml 495 Bytes 2fb97ad4 over 1 year Pierre-Loïc Garoche Merge conflict solved
verifiers.ml 1.22 KB 2fb97ad4 over 1 year Pierre-Loïc Garoche Merge conflict solved
version.ml.in 155 Bytes a86bae77 over 2 years Pierre-Loïc Garoche - Adding new Makefile target for regression tes...

Latest revisions

# Date Author Comment
81229f63 07/11/2019 06:39 AM Pierre-Loïc Garoche

Seal-extract: first serious version. Guards are gathered as a single expression

3b7f916b 07/10/2019 09:16 PM Pierre-Loïc Garoche

Updated version seal-extract

47851ec2 07/09/2019 03:02 AM Pierre-Loïc Garoche

Working version of seal-extract. Heavy load on z3.
TODO: improvement through memoization

7659bbb1 07/09/2019 03:02 AM Pierre-Loïc Garoche

Corelang function: push_negations that propagate negations in leafs of the expression

7aaacbc9 07/07/2019 03:24 AM Pierre-Loïc Garoche

Better extraction in lustrev-seal

58301109 07/07/2019 03:24 AM Pierre-Loïc Garoche

Zustre: Bug solved in const injection for reals

2104c80a 07/06/2019 12:49 AM Pierre-Loïc Garoche

Addressed a TODO in MCDC Pathconditions: simpler condition for single expression

df94cd73 07/06/2019 12:04 AM Pierre-Loïc Garoche

- More systematic translation for mutation
- copy_var_decl now keeps the generated type

e998fc16 07/05/2019 11:15 PM Pierre-Loïc Garoche

Mutation translates now ids in cocospec import

67ef9395 07/04/2019 05:35 PM Pierre-Loïc Garoche

minor bugs solved in printer: guarantee vs guarantees in cocospec. Imported node shall not be printed as regular code since it is not part of the grammar yet. Kept them as comment.

View revisions

Also available in: Atom