Project

General

Profile

Activity

From 09/27/2021 to 10/26/2021

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

10/13/2021

06:42 PM Revision a56f563e (lustrec): more compact assign clauses for state variables, and remove useless memory pack predicates and assertions
Lélio Brun

10/07/2021

06:34 PM Revision 0da3f528 (lustrec): remove tests with include directives
Lélio Brun
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 Lélio Brun
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)
Lélio Brun
10:30 AM Revision d119be37 (lustrec): fix test script
Lélio Brun

10/06/2021

06:32 PM Revision 74ebe1f9 (lustrec): fix bug in handling state variables in nested expressions
Lélio Brun
06:04 PM Revision 4240dfcb (lustrec): add basic support to protect against some ACSL keywords
Lélio Brun
05:12 PM Revision e164da10 (lustrec): fix live variable calculation for spec: take variables occuring in clocks into account
Lélio Brun
12:52 PM Revision fb6e2cfd (lustrec): print (*mem) instead of *mem to avoid ambiguities with accesses
Lélio Brun
11:25 AM Revision e77a0fa5 (lustrec): fix handling of state variables in spec expressions
Lélio Brun
10:18 AM Revision 81d69074 (lustrec): fix bug where singleton tuples were generated
Lélio Brun

10/05/2021

01:59 PM Revision 569e560f (lustrec): test everything
Lélio Brun
01:55 PM Revision 9c227bad (lustrec): fix offline tests
Lélio Brun
11:17 AM Revision 10131419 (lustrec): add offline tests and fix a bug in generated spec where optimization was not performed
Lélio Brun

10/01/2021

01:46 PM Revision b2ad5de3 (lustrec): fix tests procedure
Lélio Brun

09/30/2021

09:59 AM Revision d10d0cd9 (lustrec): Docker files
Lélio Brun

09/27/2021

06:00 PM Revision 89fd79f0 (lustrec): a working version for automata with 'last' case of enums as default case
Lélio Brun
01:36 PM Revision d29fbec5 (lustrec): working version for stateful contracts
Lélio Brun
 

Also available in: Atom