Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec/src/backends/C @ e164af45

Name Size Revision Age Author Comment
c_backend.ml 6.39 KB d978c46e almost 4 years Lélio Brun start instrumenting the main C function
c_backend.mli 171 Bytes cc852504 almost 4 years Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
c_backend_cmake.ml 4.14 KB d978c46e almost 4 years Lélio Brun start instrumenting the main C function
c_backend_cmake.mli 0 Bytes 50a8778a almost 4 years Lélio Brun refactoring first step
c_backend_common.ml 39.1 KB 5b98398a almost 4 years Lélio Brun first version working with stateless contracts
c_backend_common.mli 7.22 KB 5b98398a almost 4 years Lélio Brun first version working with stateless contracts
c_backend_header.ml 13.5 KB 5b98398a almost 4 years Lélio Brun first version working with stateless contracts
c_backend_header.mli 634 Bytes 18dada08 almost 4 years Lélio Brun working spec in the main function
c_backend_main.ml 14 KB 18dada08 almost 4 years Lélio Brun working spec in the main function
c_backend_main.mli 577 Bytes 18dada08 almost 4 years Lélio Brun working spec in the main function
c_backend_makefile.ml 4.78 KB d978c46e almost 4 years Lélio Brun start instrumenting the main C function
c_backend_makefile.mli 465 Bytes d978c46e almost 4 years Lélio Brun start instrumenting the main C function
c_backend_mauve.ml 7.57 KB d978c46e almost 4 years Lélio Brun start instrumenting the main C function
c_backend_mauve.mli 255 Bytes cc852504 almost 4 years Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
c_backend_spec.ml 50.4 KB e164af45 over 3 years Lélio Brun working version with additional asserts to make...
c_backend_spec.mli 198 Bytes d978c46e almost 4 years Lélio Brun start instrumenting the main C function
c_backend_src.ml 34.5 KB e164af45 over 3 years Lélio Brun working version with additional asserts to make...
c_backend_src.mli 897 Bytes e164af45 over 3 years Lélio Brun working version with additional asserts to make...

Latest revisions

# Date Author Comment
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
5b98398a 07/29/2021 04:02 PM Lélio Brun

first version working with stateless contracts
f1518c7c 07/05/2021 03:42 PM Lélio Brun

more precise spec for stdout
18dada08 07/01/2021 01:56 PM Lélio Brun

working spec in the main function
d978c46e 06/30/2021 06:10 PM Lélio Brun

start instrumenting the main C function
cc852504 06/30/2021 11:21 AM Lélio Brun

comment dead code with (* XXX: UNUSED *) disclaimer
a7062da6 06/28/2021 09:52 PM Lélio Brun

another step towards refactoring

View revisions

Also available in: Atom