[Horn] Workaround to prevent the use of declared keywords as node name

src/backends/Horn/horn_backend.ml

@@ -111,7 +111,16 @@ let check_sfunction mannot =
      end
   | _::_ -> false
 
+let preprocess machines =
+  List.fold_right (fun m res ->
+    if List.mem m.mname.node_id registered_keywords then
+      { m with mname  = { m.mname with node_id = protect_kwd m.mname.node_id }}::res
+       else
+	m :: res
+  ) machines []
+     
 let translate fmt basename prog machines=
+  let machines = preprocess machines in
   (* We print typedef *)
   print_dep fmt prog; (*print static library e.g. math*)
   print_type_definitions fmt;

src/backends/Horn/horn_backend_common.ml

@@ -47,6 +47,22 @@ let pp_conj pp fmt l =
 
 
 
+(********************************************************************************************)
+(*                    Workaround to prevent the use of declared keywords as node name       *)
+(********************************************************************************************)
+let registered_keywords = ["implies"]
+
+let protect_kwd s = 
+  if List.mem s registered_keywords then
+    "__" ^ s
+  else
+    s
+
+let node_name n =
+  let name = node_name n in
+  protect_kwd name
+
+
 let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
 let rename f = (fun v -> {v with var_id = f v.var_id } )
 let rename_machine p = rename (fun n -> concat p n)

src/backends/Horn/horn_backend_printers.ml

@@ -21,8 +21,7 @@ open Corelang
 open Machine_code
 
 open Horn_backend_common
-
-
+  
 (********************************************************************************************)
 (*                    Instruction Printing functions                                        *)
 (********************************************************************************************)