Project

General

Profile

Statistics
| Branch: | Tag: | Revision:
Name Size Revision Age Author Comment
  Ada 75c459f4 about 1 year Lélio Brun start with Spec AST generation
  C 9d693675 about 1 year Lélio Brun the generation of ACSL from machine code reveal...
  EMF 7ee5f69e about 1 year Lélio Brun corrections on loggers + spec in AST
  Horn ca7e8027 over 1 year Lélio Brun fix almost all warnings
  Java 719ae9fd over 1 year Lélio Brun migration draft on dune
  VHDL dea84f9e almost 4 years Pierre-Loïc Garoche Working example!
backends.ml 1.18 KB f69e7ea2 about 1 year Lélio Brun add -O -1 flag to disable fusion of conditionals

Latest revisions

# Date Author Comment
75c459f4 05/04/2021 06:24 PM Lélio Brun

start with Spec AST generation

f69e7ea2 05/04/2021 10:58 AM Lélio Brun

add -O -1 flag to disable fusion of conditionals

7ee5f69e 05/04/2021 10:20 AM Lélio Brun

corrections on loggers + spec in AST

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

View revisions

Also available in: Atom