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.mli
37 37
val pp_access :  printer -> printer -> formatter -> unit
38 38
val pp_call : formatter -> (printer*(printer list list)) -> unit
39 39
val pp_old : printer -> printer
40
val pp_adastring : printer -> printer
41

  
42
val pp_or : (printer list) -> printer
43
val pp_and : (printer list) -> printer
40 44

  
41 45
(* declaration printer *)
42 46
val pp_package : printer -> printer list -> bool -> formatter -> printer -> unit
......
44 48
val pp_type_decl : printer -> visibility -> printer
45 49
val pp_record : printer -> formatter -> ada_var_decl list list -> unit
46 50
val pp_procedure : printer -> (ada_var_decl list list) -> ada_with -> formatter -> def_content -> unit
47
val pp_predicate : printer -> (ada_var_decl list list) -> formatter -> ((((printer*printer) list)*(printer list)) option) -> unit
48

  
51
val pp_predicate : printer -> (ada_var_decl list list) -> formatter -> (printer option) -> unit
49 52
(* Local function :
50 53

  
51 54
val pp_parameter_mode : formatter -> parameter_mode -> unit

Also available in: Unified diff