Project

General

Profile

« Previous | Next » 

Revision f1518c7c

Added by LĂ©lio Brun over 3 years ago

more precise spec for stdout

View differences:

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