Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec/src/backends @ a56f563e

Name Size Revision Age Author Comment
  Ada d29fbec5 over 3 years Lélio Brun working version for stateful contracts
  C a56f563e over 3 years Lélio Brun more compact assign clauses for state variables...
  EMF dccec723 over 3 years Lélio Brun a version that almost work for the k-inuctive t...
  Horn d29fbec5 over 3 years Lélio Brun working version for stateful contracts
  Java d978c46e over 3 years Lélio Brun start instrumenting the main C function
  VHDL d978c46e over 3 years Lélio Brun start instrumenting the main C function
backends.ml 1.17 KB d29fbec5 over 3 years Lélio Brun working version for stateful contracts
backends.mli 149 Bytes cc852504 over 3 years Lélio Brun comment dead code with (* XXX: UNUSED *) discla...

Latest revisions

# Date Author Comment
a56f563e 10/13/2021 06:42 PM Lélio Brun

more compact assign clauses for state variables, and remove useless memory pack predicates and assertions
3d1f9d9f 10/07/2021 01:27 PM Lélio Brun

more agressive optim propagation in spec in order to remove unecessarry existential variables that were eliminated (helps the solvers)
74ebe1f9 10/06/2021 06:32 PM Lélio Brun

fix bug in handling state variables in nested expressions
4240dfcb 10/06/2021 06:04 PM Lélio Brun

add basic support to protect against some ACSL keywords
fb6e2cfd 10/06/2021 12:52 PM Lélio Brun

print (*mem) instead of *mem to avoid ambiguities with accesses
e77a0fa5 10/06/2021 11:25 AM Lélio Brun

fix handling of state variables in spec expressions
81d69074 10/06/2021 10:18 AM Lélio Brun

fix bug where singleton tuples were generated
9c227bad 10/05/2021 01:55 PM Lélio Brun

fix offline tests
10131419 10/05/2021 11:17 AM Lélio Brun

add offline tests and fix a bug in generated spec where optimization was not performed
b2ad5de3 10/01/2021 01:46 PM Lélio Brun

fix tests procedure

View revisions

Also available in: Atom