Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec/src/backends/C @ b2ad5de3

Name Size Revision Age Author Comment
c_backend.ml 6.39 KB d978c46e over 3 years Lélio Brun start instrumenting the main C function
c_backend.mli 171 Bytes cc852504 over 3 years Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
c_backend_cmake.ml 4.14 KB d29fbec5 over 3 years Lélio Brun working version for stateful contracts
c_backend_cmake.mli 0 Bytes 50a8778a over 3 years Lélio Brun refactoring first step
c_backend_common.ml 39.4 KB b2ad5de3 over 3 years Lélio Brun fix tests procedure
c_backend_common.mli 7.33 KB 4fef1a04 over 3 years Lélio Brun proper generation of stateful contracts
c_backend_header.ml 13.6 KB d29fbec5 over 3 years Lélio Brun working version for stateful contracts
c_backend_header.mli 634 Bytes 18dada08 over 3 years Lélio Brun working spec in the main function
c_backend_main.ml 14 KB d29fbec5 over 3 years Lélio Brun working version for stateful contracts
c_backend_main.mli 577 Bytes 18dada08 over 3 years Lélio Brun working spec in the main function
c_backend_makefile.ml 5.08 KB b2ad5de3 over 3 years Lélio Brun fix tests procedure
c_backend_makefile.mli 580 Bytes b2ad5de3 over 3 years Lélio Brun fix tests procedure
c_backend_mauve.ml 7.57 KB d978c46e over 3 years Lélio Brun start instrumenting the main C function
c_backend_mauve.mli 255 Bytes cc852504 over 3 years Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
c_backend_spec.ml 54.9 KB b2ad5de3 over 3 years Lélio Brun fix tests procedure
c_backend_spec.mli 198 Bytes d978c46e over 3 years Lélio Brun start instrumenting the main C function
c_backend_src.ml 34.8 KB 89fd79f0 over 3 years Lélio Brun a working version for automata with 'last' case...
c_backend_src.mli 901 Bytes d29fbec5 over 3 years Lélio Brun working version for stateful contracts

Latest revisions

# Date Author Comment
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
d29fbec5 09/27/2021 01:36 PM Lélio Brun

working version for stateful contracts
4fef1a04 09/23/2021 05:51 PM Lélio Brun

proper generation of stateful contracts
478edbed 09/23/2021 04:40 PM Lélio Brun

proper handling of stateless nodes and automata
0988cb68 09/23/2021 03:40 PM Lélio Brun

proper inductive case and no code generated for contracts
e164af45 09/21/2021 11:23 AM Lélio Brun

working version with additional asserts to make the axiom work
dccec723 09/20/2021 06:46 PM Lélio Brun

a version that almost work for the k-inuctive two_counters example
f51926b8 09/07/2021 04:10 PM Lélio Brun

no need to reschedule in order to "clock-protect" the unitialized state variables in ACSL !
70710795 08/25/2021 12:00 PM Lélio Brun

first draft with translated cocospec

View revisions

Also available in: Atom