Project

General

Profile

« Previous | Next » 

Revision 97602f7c

Added by Guillaume Davy over 9 years ago

Correct bug when there is no precondition and change reprensentation
of boolean in ACSL

View differences:

tcm_benchmarks/ALT2/ALT2_proof/makefile
1 1
NAME=ALT_2.lustrec
2 2
NODE=AltitudeControl
3
PAR=1
3
PAR=4
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
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
	make -C ../../../
7 8
	../../../main_lustre_compiler.native -acsl-proof -node $(NODE) ../../$(NAME).lus
8 9

  
9 10
gui:

Also available in: Unified diff