Project

General

Profile

Statistics
| Branch: | Tag: | Revision:
Name Size Revision Age Author Comment
c_backend.ml 6.45 KB 4240dfcb over 2 years Lélio Brun add basic support to protect against some ACSL ...
c_backend.mli 171 Bytes cc852504 almost 3 years Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
c_backend_cmake.ml 4.14 KB d29fbec5 over 2 years Lélio Brun working version for stateful contracts
c_backend_cmake.mli 0 Bytes 50a8778a almost 3 years Lélio Brun refactoring first step
c_backend_common.ml 39.4 KB 74ebe1f9 over 2 years Lélio Brun fix bug in handling state variables in nested e...
c_backend_common.mli 7.35 KB e77a0fa5 over 2 years Lélio Brun fix handling of state variables in spec express...
c_backend_header.ml 13.6 KB d29fbec5 over 2 years Lélio Brun working version for stateful contracts
c_backend_header.mli 634 Bytes 18dada08 almost 3 years Lélio Brun working spec in the main function
c_backend_main.ml 14 KB d29fbec5 over 2 years Lélio Brun working version for stateful contracts
c_backend_main.mli 577 Bytes 18dada08 almost 3 years Lélio Brun working spec in the main function
c_backend_makefile.ml 5.08 KB b2ad5de3 over 2 years Lélio Brun fix tests procedure
c_backend_makefile.mli 580 Bytes b2ad5de3 over 2 years Lélio Brun fix tests procedure
c_backend_mauve.ml 7.57 KB d978c46e almost 3 years Lélio Brun start instrumenting the main C function
c_backend_mauve.mli 255 Bytes cc852504 almost 3 years Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
c_backend_spec.ml 58.7 KB 3d1f9d9f over 2 years Lélio Brun more agressive optim propagation in spec in ord...
c_backend_spec.mli 293 Bytes 4240dfcb over 2 years Lélio Brun add basic support to protect against some ACSL ...
c_backend_src.ml 34.8 KB 89fd79f0 over 2 years Lélio Brun a working version for automata with 'last' case...
c_backend_src.mli 901 Bytes d29fbec5 over 2 years Lélio Brun working version for stateful contracts

Latest revisions

# Date Author Comment
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

89fd79f0 09/27/2021 06:00 PM Lélio Brun

a working version for automata with 'last' case of enums as default case

View revisions

Also available in: Atom