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/misc_lustre_function.ml
271 271
              }
272 272
            in
273 273
            let mkval_var id = {
274
                              value_desc   = Var id;
275
                              value_type   = id.var_type;
276
                              value_annot  = None
277
                            }
274
              value_desc   = Var id;
275
              value_type   = id.var_type;
276
              value_annot  = None
277
            }
278 278
            in
279 279
            let rec find_split s1 id1 accu = function
280 280
              | [] -> [], accu, mkval_var id1

Also available in: Unified diff