Revision a6974c82
Added by Pierre-Loïc Garoche over 7 years ago
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
[Horn] Workaround to prevent the use of declared keywords as node name