Revision 4174a469
Added by Guillaume Davy almost 10 years ago
| src/backends/C/c_backend_proof.ml | ||
|---|---|---|
| 573 | 573 |
(pp_acsl_val mem1 (pp_acsl_var_read "" [])) y |
| 574 | 574 |
mem2 i |
| 575 | 575 |
| MStep (il, i, vl) -> |
| 576 |
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
|
|
| 576 |
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 "" pointer)) x in
|
|
| 577 | 577 |
pp_acsl_fun ("Ctrans_"^(node_name (fst (List.assoc i m.mcalls)))) fmt
|
| 578 | 578 |
((List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_val_type x)*) pp_val x) vl)@ |
| 579 |
(List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read "" []) x) il)@
|
|
| 579 |
(List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read "" pointer) x) il)@
|
|
| 580 | 580 |
(try ignore(List.assoc i m.minstances);[(fun fmt->fprintf fmt "%s.%s" mem1 i);(fun fmt->fprintf fmt "%s.%s" mem2 i)] with Not_found -> [])) |
| 581 | 581 |
| MBranch (g,hl) -> assert false |
| 582 | 582 |
in |
| ... | ... | |
| 585 | 585 |
| MLocalAssign (i,v) -> [fun fmt -> if List.exists (fun o -> o.var_id = i.var_id) pointer |
| 586 | 586 |
then fprintf fmt "*%s" i.var_id |
| 587 | 587 |
else fprintf fmt "%s" i.var_id] |
| 588 |
| MStateAssign (i,v) -> [fun fmt -> fprintf fmt "%a" (pp_acsl_val mem2 (pp_acsl_var_read "" pointer)) (StateVar i)]
|
|
| 588 |
| MStateAssign (i,v) -> [fun fmt -> fprintf fmt "%s._reg.%s" mem2 i.var_id]
|
|
| 589 | 589 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> [fun fmt -> fprintf fmt "%a" (pp_acsl_var_read "" pointer) i0] |
| 590 | 590 |
| MStep ([i0], i, [x;y]) when (not (Basic_library.is_internal_fun i)) && (node_name (fst (List.assoc i m.mcalls)) = "_arrow") -> |
| 591 | 591 |
[fun fmt-> fprintf fmt "%t, %s.%s" (fun fmt -> if List.exists (fun o -> o.var_id = i0.var_id) pointer |
| ... | ... | |
| 746 | 746 |
*) |
| 747 | 747 |
|
| 748 | 748 |
let pp_coq_goal name goalname code fmt = |
| 749 |
fprintf fmt "Goal %t.\nProof.\n%aQed.\n\n" (fun fmt-> fprintf fmt goalname name) code name
|
|
| 749 |
fprintf fmt "Goal %t.\nProof.\n%aQed.\n\n" goalname code name
|
|
| 750 | 750 |
|
| 751 | 751 |
let pp_coq stateless fmt m = |
| 752 | 752 |
match m.mspec with |
| 753 | 753 |
| Some _ -> |
| 754 | 754 |
let name = m.mname.node_id in |
| 755 | 755 |
if name <> arrow_id then ( |
| 756 |
pp_coq_goal name "typed_%s_step_post" pp_code_inv fmt; |
|
| 757 |
pp_coq_goal name "typed_ref_%s_step_post" pp_code_inv fmt; |
|
| 758 |
pp_coq_goal name "typed_lemma_inv_inv_%s" (pp_code_inv_inv m) fmt |
|
| 756 |
pp_coq_goal name (fun fmt -> fprintf fmt "typed_%s_step_post" name) pp_code_inv fmt; |
|
| 757 |
pp_coq_goal name (fun fmt -> fprintf fmt "typed_ref_%s_step_post" name) pp_code_inv fmt; |
|
| 758 |
pp_coq_goal name (fun fmt -> fprintf fmt "typed_lemma_inv_inv_%s" name) (pp_code_inv_inv m) fmt; |
|
| 759 |
pp_coq_goal name (fun fmt -> fprintf fmt "typed_ref_lemma_missing") (fun fmt name-> fprintf fmt "admit.\n") fmt |
|
| 759 | 760 |
) |
| 760 | 761 |
| _ -> () |
| 761 | 762 |
|
| src/backends/C/c_backend_spec.ml | ||
|---|---|---|
| 354 | 354 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 |
| 355 | 355 |
| _ -> raise (Failure ("No ACSL printer for function " ^ i))
|
| 356 | 356 |
|
| 357 |
let pp_acsl_tag fmt t = |
|
| 358 |
pp_print_string fmt (if t = Corelang.tag_true then "\\true" else if t = Corelang.tag_false then "\\false" else t) |
|
| 359 |
let rec pp_acsl_const fmt c = |
|
| 360 |
match c with |
|
| 361 |
| Const_int i -> pp_print_int fmt i |
|
| 362 |
| Const_real r -> pp_print_string fmt r |
|
| 363 |
| Const_float r -> pp_print_float fmt r |
|
| 364 |
| Const_tag t -> pp_acsl_tag fmt t |
|
| 365 |
| Const_array ca -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca
|
|
| 366 |
| Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl
|
|
| 367 |
| Const_string _ -> assert false (* string occurs in annotations not in C *) |
|
| 357 | 368 |
|
| 358 | 369 |
let rec pp_acsl_val ?(is_lhs=false) self pp_var fmt v = |
| 359 | 370 |
match v with |
| 360 |
| Cst c -> pp_c_const fmt c
|
|
| 371 |
| Cst c -> pp_acsl_const fmt c
|
|
| 361 | 372 |
| Array _ |
| 362 | 373 |
| Access _ -> assert false (* no arrays *) |
| 363 | 374 |
| Power (v, n) -> assert false |
| 364 | 375 |
| LocalVar v -> pp_var fmt v |
| 365 | 376 |
| StateVar v -> |
| 366 |
if Types.is_array_type v.var_type |
|
| 377 |
(match (Types.repr v.var_type).Types.tdesc with |
|
| 378 |
| Types.Tbool -> fprintf fmt "((%t)?\\true:\\false)" |
|
| 379 |
| _ -> fprintf fmt "%t") |
|
| 380 |
(if Types.is_array_type v.var_type |
|
| 367 | 381 |
then assert false |
| 368 |
else fprintf fmt "%s%s_reg.%s" self |
|
| 369 |
(if !Options.no_pointer then "." else "->") v.var_id |
|
| 382 |
else fun fmt -> fprintf fmt "%s%s_reg.%s" self
|
|
| 383 |
(if !Options.no_pointer then "." else "->") v.var_id)
|
|
| 370 | 384 |
| Fun (n, vl) -> Format.fprintf fmt "%a" (basic_lib_pp_acsl n Machine_code.get_val_type (pp_acsl_val self pp_var)) vl |
| 371 | 385 |
|
| 372 | 386 |
|
| ... | ... | |
| 446 | 460 |
assert false (* no array *) |
| 447 | 461 |
else ( |
| 448 | 462 |
(if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *) |
| 449 |
then fprintf fmt "(*%s%s" id.var_id suffix
|
|
| 463 |
then fprintf fmt "((*%s)%s" id.var_id suffix
|
|
| 450 | 464 |
else fprintf fmt "(%s%s" id.var_id suffix); |
| 451 | 465 |
match (Types.repr id.var_type).Types.tdesc with |
| 452 | 466 |
| Types.Tbool -> fprintf fmt "?\\true:\\false)" |
| tcm_benchmarks/ALT2/ALT2_proof/ALT_2.lustrec.c | ||
|---|---|---|
| 3 | 3 |
#include "ALT_2.lustrec.h" |
| 4 | 4 |
|
| 5 | 5 |
/* C code generated by main_lustre_compiler.native |
| 6 |
SVN version number 367
|
|
| 6 |
SVN version number 393
|
|
| 7 | 7 |
Code is C99 compliant */ |
| 8 | 8 |
|
| 9 | 9 |
/* Imported nodes declarations */ |
| tcm_benchmarks/ALT2/ALT2_proof/ALT_2.lustrec.coq | ||
|---|---|---|
| 1 |
Goal typed_AltitudeControl_step_post. |
|
| 2 |
Proof. |
|
| 3 |
intros. |
|
| 4 |
eapply Q_inv_inv_AltitudeControl. |
|
| 5 |
Focus 4. |
|
| 6 |
eassumption. |
|
| 7 |
eassumption. |
|
| 8 |
eassumption. |
|
| 9 |
eassumption. |
|
| 10 |
Qed. |
|
| 1 |
(* Generated by Frama-C WP *) |
|
| 11 | 2 |
|
| 12 |
Goal typed_ref_AltitudeControl_step_post.
|
|
| 3 |
Goal typed_AltitudeControl_step_post. |
|
| 13 | 4 |
Proof. |
| 14 | 5 |
intros. |
| 15 | 6 |
eapply Q_inv_inv_AltitudeControl. |
| ... | ... | |
| 206 | 197 |
eassumption. |
| 207 | 198 |
Qed. |
| 208 | 199 |
|
| 200 |
Goal typed_ref_AltitudeControl_step_post. |
|
| 201 |
Proof. |
|
| 202 |
intros. |
|
| 203 |
eapply Q_inv_inv_AltitudeControl. |
|
| 204 |
Focus 4. |
|
| 205 |
eassumption. |
|
| 206 |
eassumption. |
|
| 207 |
eassumption. |
|
| 208 |
eassumption. |
|
| 209 |
Qed. |
|
| 210 |
|
|
| 211 |
Goal typed_ref_AltitudeControl_step_stmt_post_20. |
|
| 212 |
Hint AltitudeControl_step,default,property. |
|
| 213 |
Proof. |
|
| 214 |
Require Why3. intros. hnf. repeat split;try why3 "CVC3" timelimit 10;try why3 "Z3" timelimit 10;try why3 "CVC4" timelimit 10. |
|
| 215 |
why3 "alt-ergo" timelimit 20. |
|
| 216 |
Qed. |
|
| 217 |
|
|
| 218 |
Goal typed_ref_lemma_missing. |
|
| 219 |
Hint missing,property. |
|
| 220 |
Proof. |
|
| 221 |
admit. |
|
| 222 |
Qed. |
|
| 223 |
|
|
| 224 |
|
|
| tcm_benchmarks/ALT2/ALT2_proof/ALT_2.lustrec.h | ||
|---|---|---|
| 1 | 1 |
/* C code generated by main_lustre_compiler.native |
| 2 |
SVN version number 367
|
|
| 2 |
SVN version number 393
|
|
| 3 | 3 |
Code is C99 compliant */ |
| 4 | 4 |
|
| 5 | 5 |
#ifndef _ALT_2_LUSTREC |
| tcm_benchmarks/ALT2/ALT2_proof/makefile | ||
|---|---|---|
| 1 | 1 |
NAME=ALT_2.lustrec |
| 2 | 2 |
NODE=AltitudeControl |
| 3 | 3 |
PAR=1 |
| 4 |
LAUNCHPROVER=-wp-prover CVC4,alt-ergo,z3,coq |
|
| 4 |
LAUNCHPROVER=-wp-prover CVC3,CVC4,alt-ergo,z3,coq
|
|
| 5 | 5 |
ARGS=$(NAME).c -wp-par $(PAR) -wp-rte -wp-model ref -wp-tactic="Require Why3. intros. hnf. repeat split;try why3 \"CVC3\" timelimit 10;try why3 \"Z3\" timelimit 10;why3 \"CVC4\" timelimit 10" -wp-script $(NAME).coq -wp-no-let |
| 6 | 6 |
gen: |
| 7 | 7 |
make -C ../../../ |
Also available in: Unified diff
Correct some problem related to new bool encoding