Merging branches, disabling the specification print in Ada backend. Should be...

Merging branches, disabling the specification print in Ada backend. Should be re-enabled at some point

src/backends/Ada/ada_backend_ads.ml

@@ -117,11 +117,15 @@ struct
      @param fmt the formater to print on
      @param machine the machine
   **)
-  let pp_step_prototype_contract fmt m = pp_procedure_prototype_contract
+  let pp_step_prototype_contract fmt m =
+    ()
+      (* Temporarily disabled while waiting for the code to stabilize 
+pp_procedure_prototype_contract
         (pp_step_prototype m)
         fmt
         m.mspec
-
+       *)
+    
   (** Remove duplicates from a list according to a given predicate.
      @param eq the predicate defining equality
      @param l the list to parse

src/backends/Ada/ada_backend_common.ml

@@ -246,7 +246,7 @@ let pp_type fmt typ =
     | Types.Tbasic Types.Basic.Tint  -> pp_integer_type fmt
     | Types.Tbasic Types.Basic.Treal -> pp_float_type fmt
     | Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt
-    | Types.Tunivar _                -> pp_polymorphic_type fmt typ.tid
+    | Types.Tunivar                  -> pp_polymorphic_type fmt typ.tid
     | Types.Tbasic _                 -> eprintf "Tbasic@."; assert false (*TODO*)
     | Types.Tconst _                 -> eprintf "Tconst@."; assert false (*TODO*)
     | Types.Tclock _                 -> eprintf "Tclock@."; assert false (*TODO*)
@@ -257,8 +257,8 @@ let pp_type fmt typ =
     | Types.Tarray _                 -> eprintf "Tarray@."; assert false (*TODO*)
     | Types.Tstatic _                -> eprintf "Tstatic@.";assert false (*TODO*)
     | Types.Tlink _                  -> eprintf "Tlink@.";  assert false (*TODO*)
-    | Types.Tvar _                   -> eprintf "Tvar@.";   assert false (*TODO*)
-    | _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false (*TODO*)
+    | Types.Tvar                     -> eprintf "Tvar@.";   assert false (*TODO*)
+    (*| _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false *)
   )
 
 

src/backends/Ada/ada_backend_wrapper.ml

@@ -101,6 +101,7 @@ struct
             fprintf fmt "Ada.Text_IO.Put(\"'%a': '\");@,Float_IO.Put(%a, Fore=>0, Aft=> 15, Exp => 0);@,Ada.Text_IO.Put_Line(\"' \")"
               pp_var_name var
               pp_var_name var
+        | Types.Basic.Tstring | Types.Basic.Trat -> assert false (* Could not be the top level inputs *)
     in
 
     (* Loop instructions *)

src/modules.ml

@@ -49,7 +49,7 @@ let add_node name value =
     let itf = value.top_decl_itf in
     match value'.top_decl_desc, value.top_decl_desc with
     | ImportedNode _, Node _          when owner = owner' && itf' && (not itf) -> ()
-    | Node _        , Node _                    -> assert false; raise (Error (value.top_decl_loc, Error.Already_bound_symbol ("node " ^ name)))
+    | Node _        , Node _                    -> raise (Error (value.top_decl_loc, Error.Already_bound_symbol ("node " ^ name)))
     | _                                         -> assert false
   with
     Not_found                                   -> update_node name value