Project

General

Profile

Activity

From 10/14/2021 to 11/12/2021

11/10/2021

09:34 AM Revision 561d6104 (lustrec): fix tests
Lélio Brun
09:34 AM Revision 34cdfc15 (lustrec): update docker with re library and tokei
Lélio Brun

11/09/2021

02:58 PM Revision f3143835 (lustrec): change shell test by a magnificent OCaml test
Lélio Brun
02:57 PM Revision f78400f5 (lustrec): fix optimizations
Lélio Brun

11/06/2021

01:50 PM Revision 33e90985 (lustrec): do not remove spec of removed assignments by optim
Lélio Brun
01:18 PM Revision cdd3eb15 (lustrec): unused vars have to be computed from both outputs AND state vars!
Lélio Brun

11/05/2021

04:29 PM Revision b6086e1a (lustrec): do not run all provers
Lélio Brun
12:38 PM Revision 7cc1f808 (lustrec): add timeout to tests
Lélio Brun
10:05 AM Revision 0eac70b4 (lustrec): remove test
Lélio Brun
10:04 AM Revision 2596633b (lustrec): replace ghost vars by universal vars in contracts
Lélio Brun

11/04/2021

03:19 PM Revision 5b15f142 (lustrec): fix tests
Lélio Brun
03:17 PM Revision 43822c59 (lustrec): ignore some tests
Lélio Brun

11/03/2021

12:47 PM Revision 1b91335d (lustrec): ignore DRAGON* tests
Lélio Brun
12:43 PM Revision 32e74d70 (lustrec): remove test
Lélio Brun
12:42 PM Revision 6ab6d6de (lustrec): move asserts eqs at the end to respect dependencies
Lélio Brun
12:22 PM Revision d4870b2f (lustrec): do not eliminate vars in transitions defs but eliminate constants
Lélio Brun
11:22 AM Revision 238a8491 (lustrec): add integer casts in ACSL
Lélio Brun
11:21 AM Revision f3ff1a98 (lustrec): since the df optim backward optim has been disabled, elimination is in a fixpoint now so elim chains are taken into account
Lélio Brun

11/02/2021

07:03 PM Revision 20495fd2 (lustrec): add ignored tests possibility
Lélio Brun
06:06 PM Revision 2edea2e6 (lustrec): replace the Reset: label by a ghost variable
Lélio Brun

10/29/2021

04:17 PM Revision 2767740d (lustrec): use ghost variables instead of existential variables to avoid read / write capture problems with variable reuse
Lélio Brun

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... Lélio Brun
05:53 PM Revision ebabd357 (lustrec): fix dependencies calculus not depending on instances in Machine
Lélio Brun

10/27/2021

06:10 PM Revision 131be1c6 (lustrec): fix spec optimization by variable reuse
Lélio Brun
05:05 PM Revision d9042c7b (lustrec): fix errors in elimination optimization and dependencies calculus in Machine code
Lélio Brun
09:47 AM Revision e25cd9e9 (lustrec): disable retro-elimination of dataflows after Machine optim
Lélio Brun

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
Lélio Brun
05:44 PM Revision 60aff95d (lustrec): normalize existentials in ACSL (seems easier for solvers)
Lélio Brun

10/22/2021

02:57 PM Revision 17d63fff (lustrec): remove unused variables after tag elimination in machine code (-O >= 3)
Lélio Brun

10/21/2021

06:32 PM Revision 134e6b64 (lustrec): remove debug line
Lélio Brun
06:32 PM Revision 53c9845b (lustrec): fix optimization for variable reuse that was not propagated in branches
Lélio Brun

10/15/2021

02:37 PM Revision ebbe2fc3 (lustrec): state variables ar not free
Lélio Brun
 

Also available in: Atom