|
1
|
NAME=ALT_2.lustrec
|
|
2
|
NODE=AltitudeControl
|
|
3
|
PAR=1
|
|
4
|
LAUNCHPROVER=-wp-prover CVC3,CVC4,alt-ergo,z3,coq
|
|
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
|
gen:
|
|
7
|
make -C ../../../
|
|
8
|
../../../main_lustre_compiler.native -acsl-proof -node $(NODE) ../../$(NAME).lus
|
|
9
|
|
|
10
|
gui:
|
|
11
|
frama-c-gui $(ARGS)
|
|
12
|
|
|
13
|
cgui:
|
|
14
|
frama-c-gui -wp $(LAUNCHPROVER) $(ARGS)
|
|
15
|
|
|
16
|
check:
|
|
17
|
frama-c -wp $(LAUNCHPROVER) $(ARGS)
|
|
18
|
|
|
19
|
framac: gui
|
|
20
|
|
|
21
|
# -wp-no-bits -wp-no-clean -wp-no-let -wp-no-pruning -wp-no-simpl
|
|
22
|
|
|
23
|
#-wp-bits Use bit-test simplifications (by default). (set by
|
|
24
|
# default, opposite option is -wp-no-bits)
|
|
25
|
#-wp-clean Use variable filtering (by default). (set by default,
|
|
26
|
# opposite option is -wp-no-clean)
|
|
27
|
#-wp-dynamic Handle dynamic calls with specific annotations. (opposite
|
|
28
|
# option is -wp-no-dynamic)
|
|
29
|
#-wp-invariants Handle generalized invariants inside loops. (opposite
|
|
30
|
# option is -wp-no-invariants)
|
|
31
|
#-wp-let Use variable elimination (by default). (set by default,
|
|
32
|
# opposite option is -wp-no-let)
|
|
33
|
#-wp-pruning Prune trivial branches (by default). (set by default,
|
|
34
|
# opposite option is -wp-no-pruning)
|
|
35
|
#-wp-qed-checks Cheks internal simplifications. (opposite option is
|
|
36
|
# -wp-no-qed-checks)
|
|
37
|
#-wp-rte Generates RTE guards before WP (opposite option is
|
|
38
|
# -wp-no-rte)
|
|
39
|
#-wp-simpl Simplify constant terms and predicates. (set by default,
|
|
40
|
# opposite option is -wp-no-simpl)
|
|
41
|
#-wp-split Split conjunctions into sub-goals. (opposite option is
|
|
42
|
# -wp-no-split)
|