Activity
From 09/30/2021 to 10/29/2021
10/29/2021
10/28/2021
- 05:54 PM Revision 678a94ac (lustrec): generate existential vars to handle reuse optimization
- Discussion w Xavier: replace this mechanism (fragile because of non-constructive witnesses) with a ghost-variables-ba...
- 05:53 PM Revision ebabd357 (lustrec): fix dependencies calculus not depending on instances in Machine
10/27/2021
- 06:10 PM Revision 131be1c6 (lustrec): fix spec optimization by variable reuse
- 05:05 PM Revision d9042c7b (lustrec): fix errors in elimination optimization and dependencies calculus in Machine code
- 09:47 AM Revision e25cd9e9 (lustrec): disable retro-elimination of dataflows after Machine optim
10/26/2021
- 05:45 PM Revision 80928084 (lustrec): do not optimize too much the spec, as we want to keep the link with the dataflow node
- 05:44 PM Revision 60aff95d (lustrec): normalize existentials in ACSL (seems easier for solvers)
10/22/2021
- 02:57 PM Revision 17d63fff (lustrec): remove unused variables after tag elimination in machine code (-O >= 3)
10/21/2021
- 06:32 PM Revision 134e6b64 (lustrec): remove debug line
- 06:32 PM Revision 53c9845b (lustrec): fix optimization for variable reuse that was not propagated in branches
10/15/2021
10/13/2021
10/07/2021
- 06:34 PM Revision 0da3f528 (lustrec): remove tests with include directives
- 06:33 PM Revision 7cb1f579 (lustrec): reintroduce existential for variables that may appear free when performing substitution
- hopefully those are less problematic since they actually exists in the program as variables
- 01:27 PM Revision 3d1f9d9f (lustrec): more agressive optim propagation in spec in order to remove unecessarry existential variables that were eliminated (helps the solvers)
- 10:30 AM Revision d119be37 (lustrec): fix test script
10/06/2021
- 06:32 PM Revision 74ebe1f9 (lustrec): fix bug in handling state variables in nested expressions
- 06:04 PM Revision 4240dfcb (lustrec): add basic support to protect against some ACSL keywords
- 05:12 PM Revision e164da10 (lustrec): fix live variable calculation for spec: take variables occuring in clocks into account
- 12:52 PM Revision fb6e2cfd (lustrec): print (*mem) instead of *mem to avoid ambiguities with accesses
- 11:25 AM Revision e77a0fa5 (lustrec): fix handling of state variables in spec expressions
- 10:18 AM Revision 81d69074 (lustrec): fix bug where singleton tuples were generated
10/05/2021
- 01:59 PM Revision 569e560f (lustrec): test everything
- 01:55 PM Revision 9c227bad (lustrec): fix offline tests
- 11:17 AM Revision 10131419 (lustrec): add offline tests and fix a bug in generated spec where optimization was not performed
10/01/2021
09/30/2021
Also available in: Atom