#!/bin/sh
# Call alt-ergo via why3

frama-c							\
	-pp-annot					\
	-no-unicode					\
	-wp						\
	-wp-rte						\
	-warn-unsigned-overflow				\
	-warn-unsigned-downcast				\
	-wp-model Typed+ref				\
	-wp-prop xxx					\
	-wp-prover why3					\
	-wp-out search_n_standalone.wp_why				\
	-wp-gen search_n_standalone.c

why3							\
	prove search_n_standalone.wp_why/typed_ref/search_n_Why3_ide.why \
	-t 10						\
	--extra-config $FRAMAC_SHARE/wp/why3/why3.conf	\
	-L search_n_standalone.wp_why/typed_ref			\
	-L $FRAMAC_SHARE/wp/why3			\
	-T VCsearch_n_no_match_post_result_xxx		\
	-P alt-ergo


exit