Revision 4240dfcb
Added by Lélio Brun 10 months ago
| src/backends/C/c_backend.ml | ||
|---|---|---|
| 121 | 121 |
Header.pp_header_from_header header_fmt basename lusic.contents) |
| 122 | 122 |
|
| 123 | 123 |
let translate_to_c generate_c_header basename prog machines dependencies = |
| 124 |
let header_m, source_m, source_main_m, makefile_m = |
|
| 124 |
let header_m, source_m, source_main_m, makefile_m, machines =
|
|
| 125 | 125 |
let open Options in |
| 126 | 126 |
match !spec with |
| 127 | 127 |
| SpecNo -> |
| 128 | 128 |
( C_backend_header.((module EmptyMod : MODIFIERS_HDR)), |
| 129 | 129 |
C_backend_src.((module EmptyMod : MODIFIERS_SRC)), |
| 130 | 130 |
C_backend_main.((module EmptyMod : MODIFIERS_MAINSRC)), |
| 131 |
C_backend_makefile.((module EmptyMod : MODIFIERS_MKF)) ) |
|
| 131 |
C_backend_makefile.((module EmptyMod : MODIFIERS_MKF)), |
|
| 132 |
machines ) |
|
| 132 | 133 |
| SpecACSL -> |
| 133 | 134 |
let open C_backend_spec in |
| 134 | 135 |
( C_backend_header.((module HdrMod : MODIFIERS_HDR)), |
| 135 | 136 |
C_backend_src.((module SrcMod : MODIFIERS_SRC)), |
| 136 | 137 |
C_backend_main.((module MainMod : MODIFIERS_MAINSRC)), |
| 137 |
C_backend_makefile.((module MakefileMod : MODIFIERS_MKF)) ) |
|
| 138 |
C_backend_makefile.((module MakefileMod : MODIFIERS_MKF)), |
|
| 139 |
sanitize_machines machines) |
|
| 138 | 140 |
| SpecC -> |
| 139 | 141 |
assert false |
| 140 | 142 |
(* not implemented yet *) |
Also available in: Unified diff
add basic support to protect against some ACSL keywords