Project

General

Profile

« Previous | Next » 

Revision a6974c82

Added by Pierre-Loïc Garoche over 7 years ago

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

View differences:

src/backends/Horn/horn_backend.ml
111 111
     end
112 112
  | _::_ -> false
113 113

  
114
let preprocess machines =
115
  List.fold_right (fun m res ->
116
    if List.mem m.mname.node_id registered_keywords then
117
      { m with mname  = { m.mname with node_id = protect_kwd m.mname.node_id }}::res
118
       else
119
	m :: res
120
  ) machines []
121
     
114 122
let translate fmt basename prog machines=
123
  let machines = preprocess machines in
115 124
  (* We print typedef *)
116 125
  print_dep fmt prog; (*print static library e.g. math*)
117 126
  print_type_definitions fmt;
src/backends/Horn/horn_backend_common.ml
47 47

  
48 48

  
49 49

  
50
(********************************************************************************************)
51
(*                    Workaround to prevent the use of declared keywords as node name       *)
52
(********************************************************************************************)
53
let registered_keywords = ["implies"]
54

  
55
let protect_kwd s = 
56
  if List.mem s registered_keywords then
57
    "__" ^ s
58
  else
59
    s
60

  
61
let node_name n =
62
  let name = node_name n in
63
  protect_kwd name
64

  
65

  
50 66
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
51 67
let rename f = (fun v -> {v with var_id = f v.var_id } )
52 68
let rename_machine p = rename (fun n -> concat p n)
src/backends/Horn/horn_backend_printers.ml
21 21
open Machine_code
22 22

  
23 23
open Horn_backend_common
24

  
25

  
24
  
26 25
(********************************************************************************************)
27 26
(*                    Instruction Printing functions                                        *)
28 27
(********************************************************************************************)

Also available in: Unified diff