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_printer.ml
81 81
    (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) pp_item_list
82 82
    (Utils.pp_final_char_if_non_empty ";@," pp_item_list)
83 83

  
84
let pp_and l fmt = fprintf fmt "(%t)" (pp_group ~sep:"@ and then " l)
85
let pp_or l fmt = fprintf fmt "(%t)" (pp_group ~sep:"@ or " l)
84 86

  
85 87
let pp_ada_with fmt = function
86 88
  | None -> fprintf fmt ""
......
91 93
        fprintf fmt " Ghost%t" (Utils.pp_final_char_if_non_empty ",@," contract)
92 94
      in
93 95
      let pp_aspect aspect fmt pps = if pps = [] then fprintf fmt "" else
94
        fprintf fmt "%s => %t" aspect (pp_group ~sep:"@,and " pps)
96
        fprintf fmt "%s => %t" aspect (pp_and pps)
95 97
      in
96 98
      let pp_contract fmt = if contract = [] then fprintf fmt "" else
97
        let sep = if pres != [] && posts != [] then ",@," else "" in
98
        fprintf fmt "@,  @[<v>%a%s%a@]"
99
        let sep fmt = if pres != [] && posts != [] then fprintf fmt ",@," else fprintf fmt "" in
100
        fprintf fmt "@,  @[<v>%a%t%a@]"
99 101
          (pp_aspect "Pre") pres
100 102
          sep
101 103
          (pp_aspect "Post") posts
......
179 181
and pp_package_instanciation pp_name pp_base_name fmt instanciations =
180 182
  pp_def fmt ([], AdaPackageDecl, pp_name, [], None, (AdaPackageInstanciation (pp_base_name, instanciations)), None)
181 183

  
184
let pp_adastring pp_content fmt =
185
  fprintf fmt "\"%t\"" pp_content
186

  
182 187
(** Print the ada package introduction sentence it can be used for body and
183 188
declaration. Boolean parameter body should be true if it is a body delcaration.
184 189
   @param fmt the formater to print on
......
201 206
   @param pp_value a format printer which print the type definition
202 207
**)
203 208
let pp_type_decl pp_name visibility fmt =
204
  pp_def fmt ([], AdaType, pp_name, [], None, AdaVisibilityDefinition visibility, None)
209
  let v = match visibility with
210
    | AdaNoVisibility -> AdaNoContent
211
    | _ -> AdaVisibilityDefinition visibility
212
  in
213
  pp_def fmt ([], AdaType, pp_name, [], None, v, None)
205 214

  
206 215
let pp_record pp_name fmt var_lists =
207 216
  pp_def fmt ([], AdaType, pp_name, [], None, AdaRecord var_lists, None)
......
210 219
  pp_def fmt ([], AdaProcedure, pp_name, args, None, content, pp_with_opt)
211 220

  
212 221
let pp_predicate pp_name args fmt content_opt =
213
  let rec quantify pp_content = function
214
    | [] -> pp_content
215
    | (pp_var, pp_type)::q -> fun fmt ->
216
      fprintf fmt "for some %t in %t => (@,  @[<v>%t@])" pp_var pp_type (quantify pp_content q)
217
  in
218 222
  let content, with_st = match content_opt with
219
    | Some (locals, booleans) -> AdaSimpleContent (quantify (fun fmt -> Utils.fprintf_list ~sep:"@;and " (fun fmt pp->pp fmt) fmt booleans) locals), None
223
    | Some content -> AdaSimpleContent content, None
220 224
    | None -> AdaNoContent, Some (true, [], [])
221 225
  in
222 226
  pp_def fmt ([], AdaFunction, pp_name, args, Some pp_boolean_type, content, with_st)
223 227

  
224

  
225

  
226

  
227 228
(** Print a cleaned an identifier for ada exportation : Ada names must not start by an
228 229
    underscore and must not contain a double underscore
229 230
   @param var name to be cleaned*)

Also available in: Unified diff