Project

General

Profile

Revision d128bbd4 src/backends/Horn/horn_backend.ml

View differences:

src/backends/Horn/horn_backend.ml
97 97
 (*Check if its an sfunction*)
98 98
  match mannot with
99 99
    [] -> false
100
  | [x] -> match x.annots with
101
             [] -> false
102
            |[(key,va)] -> match key with
103
                             [] -> false
104
                           | ["c_code"] -> true
105
                           | ["matlab"] -> true
106
                           | _ -> false
107
  | _  -> false
100
  | [x] ->
101
     begin
102
       match x.annots with
103
         [] -> false
104
        |[(key,va)] ->
105
          begin
106
            match key with
107
              [] -> false
108
            | [x]  -> x == "c_code" || x =="matlab"
109
            | _ -> false
110
          end
111
        |(_,_)::_ -> false
112
     end
113
  | _::_ -> false
108 114

  
109 115
let translate fmt basename prog machines=
110 116
  (* We print typedef *)

Also available in: Unified diff