Project

General

Profile

« Previous | Next » 

Revision 4240dfcb

Added by LĂ©lio Brun 10 months ago

add basic support to protect against some ACSL keywords

View differences:

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