Project

General

Profile

Statistics
| Branch: | Tag: | Revision:
Name Size Revision Age Author Comment
c_backend.ml 6.54 KB efcc8d7f 9 months Lélio Brun move arrow spec in its own header
c_backend_cmake.ml 3.92 KB
c_backend_common.ml 30.9 KB 6d1693b9 7 months Lélio Brun work on spec generation almost done
c_backend_header.ml 16.4 KB 6d1693b9 7 months Lélio Brun work on spec generation almost done
c_backend_main.ml 12.2 KB 6d1693b9 7 months Lélio Brun work on spec generation almost done
c_backend_makefile.ml 4.51 KB 57c96fb7 11 months Lélio Brun setup tests for dune
c_backend_mauve.ml 7.35 KB ca7e8027 12 months Lélio Brun fix almost all warnings
c_backend_spec.ml 30.2 KB 6d1693b9 7 months Lélio Brun work on spec generation almost done
c_backend_src.ml 33 KB 6d1693b9 7 months Lélio Brun work on spec generation almost done

Latest revisions

# Date Author Comment
6d1693b9 06/14/2021 07:06 PM Lélio Brun

work on spec generation almost done

9d693675 04/22/2021 03:06 PM Lélio Brun

the generation of ACSL from machine code reveal too fragile as it occurs after several transformations (eg. fusion)

efcc8d7f 04/21/2021 05:15 PM Lélio Brun

move arrow spec in its own header

186e1aef 04/21/2021 01:52 PM Lélio Brun

working proto

8d2d6fa0 04/20/2021 06:51 PM Lélio Brun

Almost works!

7f03f62d 04/16/2021 11:33 AM Lélio Brun

first version that is parsed correctly by Frama-C

4b596770 04/12/2021 05:48 PM Lélio Brun

first draft: to be tested with frama-c

15c3e4e7 03/08/2021 10:58 AM Lélio Brun

generic ACSL spec generation

c226a3ba 03/01/2021 03:56 PM Lélio Brun

start generating ACSL spec

90cc3b8e 02/19/2021 11:19 AM Lélio Brun

some rewriting in C backend pretty-printer

View revisions

Also available in: Atom