Project

General

Profile

« Previous | Next » 

Revision 173a2a8f

Added by Guillaume DAVY almost 3 years ago

Ada: Lot of specification is exported in Ada. We use ghost code to store all states,
we generate the transition pridicate but also the invariant. But two problems, occured.
The first one is a visibility problem for the record which is private but must be
public for ghost variable which have to be public for specifaction. The second
problem is that the approache requires existential quantification for inputs and
locals. It works for integers and boolean but not for floats. Some complex
solution could be found like writing an iterator for floats, expanding all
local variable and store all the required inputs in ghost variable.

View differences:

src/backends/Ada/ada_backend_adb.ml
124 124
     @param fmt the formater to print on
125 125
     @param machine the machine
126 126
  **)
127
  let pp_step_definition env typed_submachines fmt (m, m_spec_opt) =
127
  let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
128 128
    let transform_local_to_state_assign instr = match instr.instr_desc with
129 129
      | MLocalAssign (ident, value) -> 
130 130
          { instr_desc = MStateAssign (ident, value);
131 131
            lustre_eq= instr.lustre_eq }
132 132
      | x -> instr
133 133
    in
134
    let spec_instrs = match m_spec_opt with
135
      | None -> []
136
      | Some m_spec -> List.map transform_local_to_state_assign m_spec.mstep.step_instrs
134
    let pp_local_ghost_list, spec_instrs = match m_spec_opt with
135
      | None -> [], []
136
      | Some m_spec ->
137
          List.map (build_pp_var_decl_local (Some (true, [], []))) (List.filter (fun x -> not (List.mem x.var_id guarantees)) m_spec.mstep.step_locals),
138
          List.map transform_local_to_state_assign m_spec.mstep.step_instrs
137 139
    in
138 140
    let pp_local_list = List.map (build_pp_var_decl_local None) (m.mstep.step_locals) in
139 141
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (m.mstep.step_instrs@spec_instrs) in
140
    let content = AdaProcedureContent ((if pp_local_list = [] then [] else [pp_local_list]), pp_instr_list) in
142
    let content = AdaProcedureContent ((if pp_local_ghost_list = [] then [] else [pp_local_ghost_list])@(if pp_local_list = [] then [] else [pp_local_list]), pp_instr_list) in
141 143
    pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
142 144

  
143 145
  (** Print the definition of the reset procedure from a machine.
......
146 148
     @param fmt the formater to print on
147 149
     @param machine the machine
148 150
  **)
149
  let pp_reset_definition env typed_submachines fmt m =
151
  let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
150 152
    let build_assign = function var ->
151 153
      mkinstr (MStateAssign (var, mk_default_value var.var_type))
152 154
    in
153
    let assigns = List.map build_assign m.mmemory in
155
    let env, memory = match m_spec_opt with
156
      | None -> env, m.mmemory
157
      | Some m_spec ->
158
          env,
159
          (m.mmemory)
160
    in
161
    let assigns = List.map build_assign memory in
154 162
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (assigns@m.minit) in
155 163
    pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt (AdaProcedureContent ([], pp_instr_list))
156 164

  
......
164 172
     @param typed_submachines list of all typed machine instances of this machine
165 173
     @param m the machine
166 174
  **)
167
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine)) =
175
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees, past_size), machine)) =
168 176
    let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
169 177
    let pp_reset fmt =
170 178
      if is_machine_statefull machine then
171
        fprintf fmt "%a;@,@," (pp_reset_definition env typed_submachines) machine
179
        fprintf fmt "%a;@,@," (pp_reset_definition env typed_submachines) (machine, opt_spec_machine)
172 180
      else
173 181
        fprintf fmt ""
174 182
    in
......
188 196
        pp_reset
189 197
        
190 198
        (*Define the step procedure*)
191
        (pp_step_definition env typed_submachines) (machine, opt_spec_machine)
199
        (pp_step_definition env typed_submachines) (machine, opt_spec_machine, guarantees)
192 200
    in
193 201
    fprintf fmt "%a%t%a;@."
194 202
      
195 203
      (* Include all the required packages*)
196
      (Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility)) packages
204
      (Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate)) packages
197 205
      (Utils.pp_final_char_if_non_empty ";@,@," packages)
198 206
      
199 207
      (*Print package*)

Also available in: Unified diff