Revision f1518c7c
Added by LĂ©lio Brun over 3 years ago
src/backends/C/c_backend_spec.ml | ||
---|---|---|
95 | 95 |
|
96 | 96 |
let pp_nothing fmt () = pp_print_string fmt "\\nothing" |
97 | 97 |
|
98 |
let pp_null fmt () = pp_print_string fmt "\\null" |
|
99 |
|
|
100 |
let pp_stdout fmt () = pp_print_string fmt "stdout" |
|
101 |
|
|
98 | 102 |
let pp_at pp_v fmt (v, l) = fprintf fmt "\\at(%a, %s)" pp_v v l |
99 | 103 |
|
100 | 104 |
let instances machines m = |
... | ... | |
201 | 205 |
pp_v |
202 | 206 |
fmt |
203 | 207 |
|
208 |
let pp_or pp_l pp_r fmt (l, r) = fprintf fmt "@[<v>%a @ || %a@]" pp_l l pp_r r |
|
209 |
|
|
204 | 210 |
let pp_or_l pp_v fmt = |
205 | 211 |
pp_print_list |
206 | 212 |
~pp_open_box:pp_open_vbox0 |
... | ... | |
212 | 218 |
|
213 | 219 |
let pp_valid pp = pp_and_l (fun fmt x -> fprintf fmt "\\valid(%a)" pp x) |
214 | 220 |
|
221 |
let pp_valid_read pp fmt = fprintf fmt "\\valid_read(%a)" pp |
|
222 |
|
|
215 | 223 |
let pp_old pp fmt = fprintf fmt "\\old(%a)" pp |
216 | 224 |
|
217 | 225 |
let pp_ite pp_c pp_t pp_f fmt (c, t, f) = |
... | ... | |
1093 | 1101 |
pp_ref' |
1094 | 1102 |
(pp_ref pp_var_decl))) |
1095 | 1103 |
(main_mem, main_mem_ghost, insts, m.mstep.step_outputs) |
1096 |
(pp_loop_invariant (pp_valid pp_print_string)) |
|
1097 |
[ "stdout" ]) |
|
1104 |
(pp_loop_invariant |
|
1105 |
(pp_or |
|
1106 |
(pp_valid_read pp_stdout) |
|
1107 |
(pp_equal pp_stdout pp_null))) |
|
1108 |
((), ((), ()))) |
|
1098 | 1109 |
fmt |
1099 | 1110 |
() |
1100 | 1111 |
|
... | ... | |
1104 | 1115 |
fprintf |
1105 | 1116 |
fmt |
1106 | 1117 |
"%a@,%a@,%a@,%a" |
1107 |
(pp_requires (pp_valid pp_print_string)) |
|
1108 |
[ "stdout" ] |
|
1118 |
(pp_requires |
|
1119 |
(pp_or |
|
1120 |
(pp_valid_read pp_stdout) |
|
1121 |
(pp_equal pp_stdout pp_null))) |
|
1122 |
((), ((), ())) |
|
1109 | 1123 |
(pp_terminates pp_false) |
1110 | 1124 |
() |
1111 | 1125 |
(pp_ensures pp_false) |
Also available in: Unified diff
more precise spec for stdout