Revision 822f31e1
Added by Teme Kahsai about 8 years ago
| autom4te.cache/requests | ||
|---|---|---|
| 14 | 14 |
'configure.ac' |
| 15 | 15 |
], |
| 16 | 16 |
{
|
| 17 |
'AC_CANONICAL_BUILD' => 1, |
|
| 18 |
'AC_SUBST' => 1, |
|
| 19 |
'AC_CONFIG_LINKS' => 1, |
|
| 20 |
'AM_MAINTAINER_MODE' => 1, |
|
| 21 |
'_AM_COND_IF' => 1, |
|
| 22 |
'_AM_MAKEFILE_INCLUDE' => 1, |
|
| 23 |
'LT_SUPPORTED_TAG' => 1, |
|
| 24 |
'LT_INIT' => 1, |
|
| 25 |
'm4_pattern_forbid' => 1, |
|
| 26 |
'AC_LIBSOURCE' => 1, |
|
| 27 |
'AM_CONDITIONAL' => 1, |
|
| 28 |
'AM_PROG_CXX_C_O' => 1, |
|
| 29 |
'm4_pattern_allow' => 1, |
|
| 30 |
'AM_INIT_AUTOMAKE' => 1, |
|
| 17 |
'_LT_AC_TAGCONFIG' => 1, |
|
| 31 | 18 |
'AM_PROG_CC_C_O' => 1, |
| 32 |
'AM_PROG_FC_C_O' => 1, |
|
| 19 |
'AM_PROG_F77_C_O' => 1, |
|
| 20 |
'AM_AUTOMAKE_VERSION' => 1, |
|
| 21 |
'AM_PROG_AR' => 1, |
|
| 22 |
'AM_GNU_GETTEXT' => 1, |
|
| 33 | 23 |
'AC_INIT' => 1, |
| 34 |
'AC_CONFIG_AUX_DIR' => 1, |
|
| 24 |
'AC_SUBST_TRACE' => 1, |
|
| 25 |
'AM_CONDITIONAL' => 1, |
|
| 26 |
'LT_CONFIG_LTDL_DIR' => 1, |
|
| 27 |
'LT_SUPPORTED_TAG' => 1, |
|
| 28 |
'AC_CANONICAL_BUILD' => 1, |
|
| 29 |
'AH_OUTPUT' => 1, |
|
| 30 |
'LT_INIT' => 1, |
|
| 31 |
'include' => 1, |
|
| 32 |
'AC_CANONICAL_SYSTEM' => 1, |
|
| 33 |
'AC_CONFIG_SUBDIRS' => 1, |
|
| 34 |
'AC_CONFIG_FILES' => 1, |
|
| 35 |
'AM_PROG_MOC' => 1, |
|
| 36 |
'AC_CANONICAL_TARGET' => 1, |
|
| 37 |
'm4_sinclude' => 1, |
|
| 38 |
'_m4_warn' => 1, |
|
| 35 | 39 |
'AM_SILENT_RULES' => 1, |
| 36 |
'AC_FC_SRCEXT' => 1, |
|
| 40 |
'AM_POT_TOOLS' => 1, |
|
| 41 |
'AM_ENABLE_MULTILIB' => 1, |
|
| 42 |
'sinclude' => 1, |
|
| 37 | 43 |
'AC_CONFIG_HEADERS' => 1, |
| 44 |
'AM_GNU_GETTEXT_INTL_SUBDIR' => 1, |
|
| 38 | 45 |
'AC_FC_FREEFORM' => 1, |
| 39 |
'm4_include' => 1, |
|
| 40 |
'sinclude' => 1, |
|
| 41 |
'AM_POT_TOOLS' => 1, |
|
| 42 |
'_m4_warn' => 1, |
|
| 43 |
'AC_CONFIG_SUBDIRS' => 1, |
|
| 44 | 46 |
'AC_CANONICAL_HOST' => 1, |
| 45 |
'LT_CONFIG_LTDL_DIR' => 1,
|
|
| 47 |
'm4_pattern_allow' => 1,
|
|
| 46 | 48 |
'AC_DEFINE_TRACE_LITERAL' => 1, |
| 47 |
'AM_AUTOMAKE_VERSION' => 1, |
|
| 48 |
'include' => 1, |
|
| 49 |
'AM_PROG_FC_C_O' => 1, |
|
| 50 |
'AM_XGETTEXT_OPTION' => 1, |
|
| 51 |
'_AM_MAKEFILE_INCLUDE' => 1, |
|
| 49 | 52 |
'AC_CONFIG_LIBOBJ_DIR' => 1, |
| 50 |
'AC_CANONICAL_TARGET' => 1, |
|
| 53 |
'AC_REQUIRE_AUX_FILE' => 1, |
|
| 54 |
'AC_LIBSOURCE' => 1, |
|
| 51 | 55 |
'AM_NLS' => 1, |
| 52 |
'AH_OUTPUT' => 1, |
|
| 53 |
'AM_PROG_MOC' => 1, |
|
| 54 |
'AC_SUBST_TRACE' => 1, |
|
| 55 |
'm4_sinclude' => 1, |
|
| 56 |
'_LT_AC_TAGCONFIG' => 1, |
|
| 57 |
'AC_FC_PP_DEFINE' => 1, |
|
| 58 |
'AC_CANONICAL_SYSTEM' => 1, |
|
| 56 |
'AM_MAINTAINER_MODE' => 1, |
|
| 59 | 57 |
'_AM_COND_ELSE' => 1, |
| 58 |
'AM_PATH_GUILE' => 1, |
|
| 59 |
'm4_pattern_forbid' => 1, |
|
| 60 |
'AC_FC_PP_DEFINE' => 1, |
|
| 61 |
'AC_CONFIG_AUX_DIR' => 1, |
|
| 60 | 62 |
'AC_PROG_LIBTOOL' => 1, |
| 61 |
'AM_PROG_AR' => 1, |
|
| 62 |
'AM_GNU_GETTEXT_INTL_SUBDIR' => 1, |
|
| 63 |
'_AM_SUBST_NOTMAKE' => 1, |
|
| 64 |
'AC_REQUIRE_AUX_FILE' => 1, |
|
| 65 |
'AM_GNU_GETTEXT' => 1, |
|
| 66 | 63 |
'_AM_COND_ENDIF' => 1, |
| 67 |
'AC_FC_PP_SRCEXT' => 1, |
|
| 68 |
'AM_ENABLE_MULTILIB' => 1, |
|
| 69 |
'AM_PATH_GUILE' => 1, |
|
| 70 |
'AC_CONFIG_FILES' => 1, |
|
| 71 |
'AM_XGETTEXT_OPTION' => 1, |
|
| 72 | 64 |
'AM_MAKEFILE_INCLUDE' => 1, |
| 73 |
'AM_PROG_F77_C_O' => 1 |
|
| 65 |
'_AM_SUBST_NOTMAKE' => 1, |
|
| 66 |
'AC_FC_SRCEXT' => 1, |
|
| 67 |
'AM_PROG_CXX_C_O' => 1, |
|
| 68 |
'm4_include' => 1, |
|
| 69 |
'_AM_COND_IF' => 1, |
|
| 70 |
'AC_FC_PP_SRCEXT' => 1, |
|
| 71 |
'AC_CONFIG_LINKS' => 1, |
|
| 72 |
'AC_SUBST' => 1, |
|
| 73 |
'AM_INIT_AUTOMAKE' => 1 |
|
| 74 | 74 |
} |
| 75 | 75 |
], 'Autom4te::Request' ) |
| 76 | 76 |
); |
| src/backends/Horn/horn_backend_printers.ml | ||
|---|---|---|
| 42 | 42 |
let rec pp_horn_const fmt c = |
| 43 | 43 |
match c with |
| 44 | 44 |
| Const_int i -> pp_print_int fmt i |
| 45 |
| Const_real r -> pp_print_string fmt r |
|
| 46 |
| Const_float r -> pp_print_float fmt r |
|
| 45 |
| Const_real (_,_,s) -> pp_print_string fmt s |
|
| 47 | 46 |
| Const_tag t -> pp_horn_tag fmt t |
| 48 | 47 |
| _ -> assert false |
| 49 | 48 |
|
| ... | ... | |
| 52 | 51 |
but an offset suffix may be added for array variables |
| 53 | 52 |
*) |
| 54 | 53 |
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v = |
| 55 |
match v with |
|
| 54 |
match v.value_desc with
|
|
| 56 | 55 |
| Cst c -> pp_horn_const fmt c |
| 57 | 56 |
| Array _ |
| 58 | 57 |
| Access _ -> assert false (* no arrays *) |
| ... | ... | |
| 66 | 65 |
|
| 67 | 66 |
(* Prints a [value] indexed by the suffix list [loop_vars] *) |
| 68 | 67 |
let rec pp_value_suffix self pp_value fmt value = |
| 69 |
match value with |
|
| 68 |
match value.value_desc with
|
|
| 70 | 69 |
| Fun (n, vl) -> |
| 71 | 70 |
Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl |
| 72 | 71 |
| _ -> |
| ... | ... | |
| 78 | 77 |
- [value]: assigned value |
| 79 | 78 |
- [pp_var]: printer for variables |
| 80 | 79 |
*) |
| 81 |
let pp_assign m pp_var fmt var_type var_name value =
|
|
| 80 |
let pp_assign m pp_var fmt var_name value = |
|
| 82 | 81 |
let self = m.mname.node_id in |
| 83 | 82 |
fprintf fmt "(= %a %a)" |
| 84 | 83 |
(pp_horn_val ~is_lhs:true self pp_var) var_name |
| ... | ... | |
| 157 | 156 |
| "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin |
| 158 | 157 |
fprintf fmt "@[<v 5>(and "; |
| 159 | 158 |
fprintf fmt "(= %a (ite %a %a %a))" |
| 160 |
(pp_horn_val ~is_lhs:true self (pp_horn_var m)) (LocalVar o) (* output var *)
|
|
| 159 |
(pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)
|
|
| 161 | 160 |
(pp_horn_var m) mem_m |
| 162 | 161 |
(pp_horn_val self (pp_horn_var m)) i1 |
| 163 | 162 |
(pp_horn_val self (pp_horn_var m)) i2 |
| ... | ... | |
| 173 | 172 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs |
| 174 | 173 |
(Utils.pp_final_char_if_non_empty "@ " inputs) |
| 175 | 174 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) |
| 176 |
(List.map (fun v -> LocalVar v) outputs)
|
|
| 175 |
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
|
|
| 177 | 176 |
(Utils.pp_final_char_if_non_empty "@ " outputs) |
| 178 | 177 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems) |
| 179 | 178 |
|
| ... | ... | |
| 187 | 186 |
inputs |
| 188 | 187 |
(Utils.pp_final_char_if_non_empty "@ " inputs) |
| 189 | 188 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) |
| 190 |
(List.map (fun v -> LocalVar v) outputs)
|
|
| 189 |
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
|
|
| 191 | 190 |
) |
| 192 | 191 |
|
| 193 | 192 |
|
| 194 | 193 |
(* Print the instruction and update the set of reset instances *) |
| 195 | 194 |
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list = |
| 196 | 195 |
match instr with |
| 196 |
| MComment _ -> reset_instances |
|
| 197 | 197 |
| MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *) |
| 198 | 198 |
pp_no_reset machines m fmt i; |
| 199 | 199 |
i::reset_instances |
| ... | ... | |
| 203 | 203 |
| MLocalAssign (i,v) -> |
| 204 | 204 |
pp_assign |
| 205 | 205 |
m (pp_horn_var m) fmt |
| 206 |
i.var_type (LocalVar i) v;
|
|
| 206 |
(mk_val (LocalVar i) i.var_type) v;
|
|
| 207 | 207 |
reset_instances |
| 208 | 208 |
| MStateAssign (i,v) -> |
| 209 | 209 |
pp_assign |
| 210 | 210 |
m (pp_horn_var m) fmt |
| 211 |
i.var_type (StateVar i) v;
|
|
| 211 |
(mk_val (StateVar i) i.var_type) v;
|
|
| 212 | 212 |
reset_instances |
| 213 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> |
|
| 213 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
|
|
| 214 | 214 |
assert false (* This should not happen anymore *) |
| 215 | 215 |
| MStep (il, i, vl) -> |
| 216 | 216 |
(* if reset instance, just print the call over mem_m , otherwise declare mem_m = |
| src/printers.ml | ||
|---|---|---|
| 143 | 143 |
(* |
| 144 | 144 |
let pp_node_var fmt id = fprintf fmt "%s%s: %a(%a)%a" (if id.var_dec_const then "const " else "") id.var_id print_dec_ty id.var_dec_type.ty_dec_desc Types.print_ty id.var_type Clocks.print_ck_suffix id.var_clock |
| 145 | 145 |
*) |
| 146 |
let pp_node_var ?(print_when=false) fmt id =
|
|
| 146 |
let pp_node_var fmt id = |
|
| 147 | 147 |
begin |
| 148 |
fprintf fmt "%s%s: %a%t%t" |
|
| 149 |
(if id.var_dec_const then "const " else "") |
|
| 150 |
id.var_id |
|
| 151 |
Types.print_node_ty id.var_type |
|
| 152 |
(fun fmt -> match id.var_dec_value with |
|
| 153 |
| None -> () |
|
| 154 |
| Some v -> fprintf fmt " = %a" pp_expr v |
|
| 155 |
) |
|
| 156 |
(fun fmt -> if print_when || not ( Clocks.is_clocked id.var_clock ) then |
|
| 157 |
fprintf fmt "%a;" |
|
| 158 |
Clocks.print_ck_suffix id.var_clock |
|
| 159 |
else |
|
| 160 |
fprintf fmt "; -- %a" |
|
| 161 |
Clocks.print_ck_suffix id.var_clock |
|
| 162 |
) |
|
| 148 |
fprintf fmt "%s%s: %a%a" (if id.var_dec_const then "const " else "") id.var_id Types.print_node_ty id.var_type Clocks.print_ck_suffix id.var_clock; |
|
| 149 |
match id.var_dec_value with |
|
| 150 |
| None -> () |
|
| 151 |
| Some v -> fprintf fmt " = %a" pp_expr v |
|
| 163 | 152 |
end |
| 164 | 153 |
|
| 165 |
let pp_node_args = fprintf_list ~sep:" " (pp_node_var ~print_when:true) |
|
| 166 |
let pp_node_var = pp_node_var ~print_when:false |
|
| 154 |
let pp_node_args = fprintf_list ~sep:"; " pp_node_var |
|
| 167 | 155 |
|
| 168 | 156 |
let pp_node_eq fmt eq = |
| 169 | 157 |
fprintf fmt "%a = %a;" |
| ... | ... | |
| 193 | 181 |
match locals with [] -> () | _ -> |
| 194 | 182 |
Format.fprintf fmt "@[<v 4>var %a@]@ " |
| 195 | 183 |
(Utils.fprintf_list ~sep:"@ " |
| 196 |
(fun fmt v -> pp_node_var fmt v))
|
|
| 184 |
(fun fmt v -> Format.fprintf fmt "%a;" pp_node_var v))
|
|
| 197 | 185 |
locals) |
| 198 | 186 |
handler.hand_locals |
| 199 | 187 |
pp_node_stmts handler.hand_stmts |
| ... | ... | |
| 286 | 274 |
match locals with [] -> () | _ -> |
| 287 | 275 |
fprintf fmt "@[<v 4>var %a@]@ " |
| 288 | 276 |
(fprintf_list ~sep:"@ " |
| 289 |
(fun fmt v -> pp_node_var fmt v))
|
|
| 277 |
(fun fmt v -> fprintf fmt "%a;" pp_node_var v))
|
|
| 290 | 278 |
locals |
| 291 | 279 |
) nd.node_locals |
| 292 | 280 |
(fun fmt checks -> |
| src/version.ml | ||
|---|---|---|
| 1 | 1 |
|
| 2 |
<<<<<<< HEAD |
|
| 3 | 2 |
let number = "1.1-Unversioned directory" |
| 4 |
======= |
|
| 5 |
let number = "1.3- 459" |
|
| 6 |
>>>>>>> onera_master |
|
| 7 | 3 |
|
| 8 |
let codename ="Xia/Zhong-Kang-dev"
|
|
| 4 |
let codename ="@VERSION_CODENAME@"
|
|
| 9 | 5 |
|
| 10 | 6 |
let prefix = "/Users/Teme/Documents/GitHub/lustrec/cocosim" |
| 11 | 7 |
|
Also available in: Unified diff
updating to onera version 30f766a:2016-12-04