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.ml
112 112
            | [] -> None
113 113
            | _ -> Some machine_spec
114 114
        in
115
        None, [] (*(opt_machine_spec, guarantees)*)
115
        (opt_machine_spec, guarantees, 4)
116 116
      end
117
    | _ -> None, []
117
    | _ -> None, [], 0
118 118

  
119 119
(** Main function of the Ada backend. It calls all the subfunction creating all
120 120
the file and fill them with Ada code representing the machines list given.

Also available in: Unified diff