Commits · bcfd6e010ad96b9552277be1ca29f9ceb170e194 · LustreC / Lustrec - public version · GitLab

Snippets Groups Projects

Mar 22, 2023
- corrected again a regression bug in causality/scheduling: bad handling of tuples · bcfd6e01
  THIRIOUX Xavier authored 2 years ago
  
  bcfd6e01
Mar 21, 2023
- restored correct inlining for constants and locals · 0f7b31bd
  THIRIOUX Xavier authored 2 years ago
  
  0f7b31bd
Mar 20, 2023
- instance counter restored · c7504a35
  THIRIOUX Xavier authored 2 years ago
  
  c7504a35
- a correct scheduling should be restored · f2c9f35a
  THIRIOUX Xavier authored 2 years ago
  
  f2c9f35a
Mar 15, 2023
- simpler structure for tracking rewrites · 34c9bffa
  BRUN Lelio authored 2 years ago
  
  34c9bffa
Mar 14, 2023
- fix introduction of '__' ghost vars in branches · ac33d091
  BRUN Lelio authored 2 years ago
  
  ac33d091
- [optimizations] remove unnecessary log printing · 8a17d52f
  GARION Christophe authored 2 years ago
  
  8a17d52f
- fix a bug where protecting ghost vars were not introduced at the proper sites · 77e37a05
  BRUN Lelio authored 2 years ago
  
  77e37a05
- apply the same fix to 'reassigned' ghost assignments · 3cb1ac88
  BRUN Lelio authored 2 years ago
  
  3cb1ac88
- Fix ghost assignments introduction in branches · 5e119a17
  BRUN Lelio authored 2 years ago
  
  5e119a17
- only print unused vars in log if there actually are unused vars · 66ea2ee7
  BRUN Lelio authored 2 years ago
  
  66ea2ee7
- restrict dead code elim to variables eliminated by the constructor elimination step · 9e3867be
  BRUN Lelio authored 2 years ago
  
  9e3867be
Mar 03, 2023
- fix a bug where some files were not generated if -acsl-spec was not present · ab1eff9c
  BRUN Lelio authored 2 years ago and GARION Christophe committed 2 years ago
  
  ab1eff9c
- follow chains of recycling for introducing ghost assigns · 27f2db72
  BRUN Lelio authored 2 years ago and GARION Christophe committed 2 years ago
  
  27f2db72
- avoid removing spec of `x = x` assignments · bcf13972
  BRUN Lelio authored 2 years ago and GARION Christophe committed 2 years ago
  
  bcf13972
- allow renaming variables named 'set' in ghost declarations · 9a8649cc
  BRUN Lelio authored 2 years ago and GARION Christophe committed 2 years ago
  
  9a8649cc
- fix removed plugins files by mistake... · 3addb23b
  BRUN Lelio authored 2 years ago
  
  3addb23b
- cope with newer Dune version · 6bb00bf6
  BRUN Lelio authored 2 years ago
  
  6bb00bf6
Mar 02, 2023
- fix a bug where some files were not generated if -acsl-spec was not present · c45fb8c1
  BRUN Lelio authored 2 years ago
  
  c45fb8c1
- follow chains of recycling for introducing ghost assigns · 4c061740
  BRUN Lelio authored 2 years ago
  
  4c061740
- avoid removing spec of `x = x` assignments · 7ef8a040
  BRUN Lelio authored 2 years ago
  
  7ef8a040
- move files from plugins directory as it seems to be used by new plugin system... · e7729134
  BRUN Lelio authored 2 years ago
```
move files from plugins directory as it seems to be used by new plugin system by Dune (that's weird)
```
  e7729134
Mar 01, 2023
- allow renaming variables named 'set' in ghost declarations · d62aa48b
  BRUN Lelio authored 2 years ago
  
  d62aa48b
Feb 20, 2023

add an exhaustivity parameter to Branch constructor in Machine Code to handle... · 6b20dc63

BRUN Lelio authored 2 years ago

add an exhaustivity parameter to Branch constructor in Machine Code to handle C switch default case optimization in case of a singleton enum

6b20dc63

Feb 10, 2023
- rewrite optim to use ghost vars instead of existential · de487020
  BRUN Lelio authored 2 years ago
  
  de487020
Jan 30, 2023
- also remove step calls if all written variables are unused · d6ee2630
  BRUN Lelio authored 2 years ago
  
  d6ee2630
Jan 26, 2023
- do not generate ghost reset functions for stateless machines · d800b9c3
  BRUN Lelio authored 2 years ago
  
  d800b9c3
Jan 17, 2023
- Monolithic reset in Spec · cb8b7a6f
  BRUN Lelio authored 2 years ago
  
  cb8b7a6f
Jul 05, 2022
- corrections to handle stateless / statefull · 241ef2a4
  BRUN Lelio authored 2 years ago
  
  241ef2a4
Jun 14, 2022
- remove some linebreaks · 1d77dc98
  BRUN Lelio authored 2 years ago
  
  1d77dc98
- use automatic rather than hard-coded variable names in main ACSL spec · 9e9a1f32
  BRUN Lelio authored 2 years ago
  
  9e9a1f32
May 25, 2022
- new way of handling contracts : use ghost contract function + contract transition relations · 5e34c383
  BRUN Lelio authored 2 years ago
  
  5e34c383
May 19, 2022
- format · e31b81e9
  BRUN Lelio authored 2 years ago
  
  e31b81e9
May 18, 2022
- ACSL ok for main loop of stateless nodes · 85a7d54a
  BRUN Lelio authored 2 years ago
  
  85a7d54a
- generate *_memory.h and *_spec.h headers · 893dcc99
  BRUN Lelio authored 2 years ago
  
  893dcc99
- rewrite k-induction predicates and lemmas · c097ab1c
  BRUN Lelio authored 2 years ago
  
  c097ab1c
May 12, 2022
- fix dune build · 3e9d5fa1
  BRUN Lelio authored 2 years ago
  
  3e9d5fa1
May 10, 2022
- reorganize internal libraries to solve execution failures for other executables than lustrec · 7f9aabea
  BRUN Lelio authored 2 years ago
  
  7f9aabea
Apr 15, 2022
- remove some unecessary files and some dead code · acc5e191
  BRUN Lelio authored 3 years ago
  
  acc5e191
Apr 13, 2022
- COSMETICS (dune build @fmt --auto-promote) · f1896ffa
  BRUN Lelio authored 3 years ago
  
  f1896ffa