Revision 71999483
Added by Pierre-Loïc Garoche about 4 years ago
| src/backends/C/c_backend_spec.ml | ||
|---|---|---|
| 129 | 129 |
|
| 130 | 130 |
*) |
| 131 | 131 |
|
| 132 |
(* TODO ACSL |
|
| 133 |
mspec are function body annotations, sush as loop invariants, acsl asserts ... *) |
|
| 134 |
let pp_mspec fmt s = () |
|
| 135 |
|
|
| 136 |
(* TODO ACSL |
|
| 137 |
Return updates machines (eg with local annotations) and acsl preamble *) |
|
| 138 |
let preprocess_acsl machines = machines, [] |
|
| 139 |
|
|
| 140 |
(* TODO: This preamble shall be a list of types, axiomatics, predicates, theorems *) |
|
| 141 |
let pp_acsl_preamble fmt preamble = |
|
| 142 |
Format.fprintf fmt ""; |
|
| 143 |
() |
|
| 132 | 144 |
(**************************************************************************) |
| 133 | 145 |
(* MAKEFILE *) |
| 134 | 146 |
(**************************************************************************) |
Also available in: Unified diff
Cleaning C backend - removing unused functiions
Preparing for coming ACSL