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_common.mli
13 13
val pp_step_procedure_name : printer
14 14
val pp_main_procedure_name : printer
15 15
val pp_polymorphic_type : int -> printer
16
val pp_past_name : int -> printer
16 17

  
17 18
val is_builtin_fun : string -> bool
18 19
val ada_supported_funs : (string*(string*string)) list
......
35 36
val build_pp_arg_step : machine_t -> (ada_var_decl list list)
36 37
val build_pp_arg_reset : machine_t -> (ada_var_decl list list)
37 38
val build_pp_state_decl_from_subinstance : parameter_mode -> ada_with -> (string * ((int * Types.type_expr) list * Machine_code_types.machine_t)) -> ada_var_decl
39
val build_pp_state_decl : parameter_mode -> ada_with -> ada_var_decl
38 40

  
39 41
val pp_machine_filename : string -> formatter -> machine_t -> unit
40 42
val pp_main_filename : formatter -> machine_t -> unit

Also available in: Unified diff