Revision bff13707
Added by Guillaume Davy over 10 years ago
| src/backends/C/c_backend_proof.ml | ||
|---|---|---|
| 158 | 158 |
(pp_acsl_val mem1 (pp_acsl_var_read [])) y |
| 159 | 159 |
self i |
| 160 | 160 |
| MStep (il, i, vl) -> |
| 161 |
let pp_val fmt x = (match get_val_type x with Types.Tbool -> fprintf fmt "((%a)?1:0)" | _ -> fprintf fmt "%a") (pp_acsl_val mem1 (pp_acsl_var_read [])) x in
|
|
| 161 |
let pp_val fmt x = (match get_val_type x with Types.Tbool -> fprintf fmt "%a" | _ -> fprintf fmt "%a") (pp_acsl_val mem1 (pp_acsl_var_read [])) x in
|
|
| 162 | 162 |
pp_acsl_fun ("Ctrans_"^(node_name (fst (List.assoc i calls)))) fmt
|
| 163 | 163 |
((List.map (fun x fmt-> fprintf fmt "%a %a" pp_cast (get_val_type x) pp_val x) vl)@ |
| 164 | 164 |
(List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read []) x) il)@ |
| ... | ... | |
| 216 | 216 |
(pp_acsl_at self s) |
| 217 | 217 |
*) |
| 218 | 218 |
|
| 219 |
(* |
|
| 220 |
Require Why3. |
|
| 221 |
intros. |
|
| 222 |
unfold P_trans_AltitudeControl. |
|
| 223 |
repeat split. |
|
| 224 |
why3 "Z3" timelimit 10. |
|
| 225 |
why3 "Z3" timelimit 10. |
|
| 226 |
why3 "Z3" timelimit 10. |
|
| 227 |
why3 "Z3" timelimit 10. |
|
| 228 |
why3 "Z3" timelimit 10. |
|
| 229 |
why3 "Z3" timelimit 10. |
|
| 230 |
why3 "Z3" timelimit 10. |
|
| 231 |
why3 "Z3" timelimit 10. |
|
| 232 |
why3 "Z3" timelimit 10. |
|
| 233 |
why3 "Z3" timelimit 10. |
|
| 234 |
why3 "Z3" timelimit 10. |
|
| 235 |
why3 "Z3" timelimit 10. |
|
| 236 |
why3 "Z3" timelimit 10. |
|
| 237 |
why3 "Z3" timelimit 10. |
|
| 238 |
why3 "Z3" timelimit 10. |
|
| 239 |
why3 "Z3" timelimit 10. |
|
| 240 |
why3 "Z3" timelimit 10. |
|
| 241 |
why3 "Z3" timelimit 10. |
|
| 242 |
assert (a_9 = F_AltitudeControl_mem_ni_1 a_6). |
|
| 243 |
why3 "Z3" timelimit 10. |
|
| 244 |
assert (a_10 = F_AltitudeControl_mem_ni_1 a_7). |
|
| 245 |
unfold F_AltitudeControl_mem_ni_1. |
|
| 246 |
unfold a_7. |
|
| 247 |
unfold Load_S_AltitudeControl_mem. |
|
| 248 |
unfold a_10. |
|
| 249 |
unfold a_8. |
|
| 250 |
unfold havoc in H36. |
|
| 251 |
unfold get. |
|
| 252 |
clear. |
|
| 253 |
rewrite <- H48. |
|
| 254 |
rewrite <- H49. |
|
| 255 |
apply H47. |
|
| 256 |
*) |
|
| 257 |
|
|
| 219 | 258 |
(* Print a transition call/decl in acsl *) |
| 220 | 259 |
let pp_acsl_fun_trans infos pre name inputs outputs suffix flag_output self flag_mem locals fmt existential = |
| 221 | 260 |
let (locals, existential) = (*([], match existential with None -> None | Some x -> Some []) else*) |
| ... | ... | |
| 230 | 269 |
in |
| 231 | 270 |
let mems = function 1 -> "Pre" | 2 -> "Here" | _ -> assert false in |
| 232 | 271 |
let pp_self_read = |
| 233 |
if flag_mem then fun i fmt-> fprintf fmt "\\at(*%s, %s)" self (mems i)
|
|
| 272 |
if flag_mem then fun i fmt-> (match i with 1 -> fprintf fmt "\\at(*%s, Pre)" self | 2 -> fprintf fmt "(*%s)" self | _ -> assert false)
|
|
| 234 | 273 |
else fun i fmt-> fprintf fmt "%s%i" self (match suffix with None -> i | Some s -> s+i-1) |
| 235 | 274 |
in |
| 236 | 275 |
let (pp_var, pp_self) = |
Also available in: Unified diff
ALT_2 working with modification made by hand