Project

General

Profile

Download (1.82 KB) Statistics
| Branch: | Tag: | Revision:
1
NAME=ALT_2.lustrec
2
NODE=AltitudeControl
3
PAR=4
4
LAUNCHPROVER=-wp-prover 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)
(4-4/4)