Commit c60dd91c authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] refactor share directory and coq compilation

parent f993c057
......@@ -1792,8 +1792,7 @@ src/plugins/wp/semantics/Typing.v: .ignore
src/plugins/wp/semantics/Values.v: .ignore
src/plugins/wp/semantics/coqide.sh: .ignore
src/plugins/wp/share/.gitignore: .ignore
src/plugins/wp/share/Makefile: CEA_WP
src/plugins/wp/share/Makefile.headers: CEA_WP
src/plugins/wp/share/Makefile.coqwp: CEA_WP
src/plugins/wp/share/Makefile.resources: CEA_WP
src/plugins/wp/share/coqwp/ArcTrigo.v: CEA_WP
src/plugins/wp/share/coqwp/Bits.v: CEA_WP
......@@ -1819,7 +1818,7 @@ src/plugins/wp/share/coqwp/int/Exponentiation.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/int/Int.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/int/MinMax.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/int/Power.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/for_drivers/ComputerOfEuclideanDivision.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/map/Map.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/map/Const.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/real/Abs.v: UNMODIFIED_WHY3
......@@ -1855,6 +1854,7 @@ src/plugins/wp/share/ergo/Vset.mlw: CEA_WP
src/plugins/wp/share/ergo/bool.Bool.mlw: MODIFIED_WHY3
src/plugins/wp/share/ergo/int.Abs.mlw: MODIFIED_WHY3
src/plugins/wp/share/ergo/int.ComputerDivision.mlw: MODIFIED_WHY3
src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw: MODIFIED_WHY3
src/plugins/wp/share/ergo/int.Int.mlw: MODIFIED_WHY3
src/plugins/wp/share/ergo/int.MinMax.mlw: MODIFIED_WHY3
src/plugins/wp/share/ergo/map.Map.mlw: MODIFIED_WHY3
......@@ -1872,39 +1872,6 @@ src/plugins/wp/share/ergo/real.Square.mlw: MODIFIED_WHY3
src/plugins/wp/share/ergo/real.Trigonometry.mlw: MODIFIED_WHY3
src/plugins/wp/share/ergo/real.Truncate.mlw: MODIFIED_WHY3
src/plugins/wp/share/install.ml: CEA_WP
src/plugins/wp/share/src/Cbits.v: .ignore
src/plugins/wp/share/src/Cmath.v: .ignore
src/plugins/wp/share/src/Makefile: CEA_WP
src/plugins/wp/share/src/Memory.v: .ignore
src/plugins/wp/share/src/Qed.v: .ignore
src/plugins/wp/share/src/Qedlib.v: CEA_WP
src/plugins/wp/share/src/Vlist.v: .ignore
src/plugins/wp/share/src/Vset.v: .ignore
src/plugins/wp/share/src/alt_ergo_why3_stdlib.drv: CEA_WP
src/plugins/wp/share/src/coq-own-realization.drv: CEA_PROPRIETARY
src/plugins/wp/share/src/filter_axioms.ml: CEA_WP
src/plugins/wp/share/why3/ArcTrigo.v: CEA_WP
src/plugins/wp/share/why3/ArcTrigo.why: CEA_WP
src/plugins/wp/share/why3/Bits.v: CEA_WP
src/plugins/wp/share/why3/Cbits.v: CEA_WP
src/plugins/wp/share/why3/Cbits.why: CEA_WP
src/plugins/wp/share/why3/Cfloat.v: CEA_WP
src/plugins/wp/share/why3/Cfloat.why: CEA_WP
src/plugins/wp/share/why3/Cint.v: CEA_WP
src/plugins/wp/share/why3/Cint.why: CEA_WP
src/plugins/wp/share/why3/Cmath.v: CEA_WP
src/plugins/wp/share/why3/ExpLog.v: CEA_WP
src/plugins/wp/share/why3/Memory.v: CEA_WP
src/plugins/wp/share/why3/Memory.why: CEA_WP
src/plugins/wp/share/why3/Qed.v: CEA_WP
src/plugins/wp/share/why3/Qed.why: CEA_WP
src/plugins/wp/share/why3/Qedlib.v: CEA_WP
src/plugins/wp/share/why3/Square.v: CEA_WP
src/plugins/wp/share/why3/Vlist.v: CEA_WP
src/plugins/wp/share/why3/Vlist.why: CEA_WP
src/plugins/wp/share/why3/Vset.v: CEA_WP
src/plugins/wp/share/why3/Vset.why: CEA_WP
src/plugins/wp/share/why3/Zbits.v: CEA_WP
src/plugins/wp/share/why3/frama_c_wp/cbits.mlw: CEA_WP
src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw: CEA_WP
src/plugins/wp/share/why3/frama_c_wp/cint.mlw: CEA_WP
......@@ -1914,7 +1881,6 @@ src/plugins/wp/share/why3/frama_c_wp/qed.mlw: CEA_WP
src/plugins/wp/share/why3/frama_c_wp/vlist.mlw: CEA_WP
src/plugins/wp/share/why3/frama_c_wp/vset.mlw: CEA_WP
src/plugins/wp/share/wp.driver: CEA_WP
src/plugins/wp/share/wpcoqdoc.zip: .ignore
src/plugins/wp/wpAnnot.ml: CEA_WP
src/plugins/wp/wpAnnot.mli: CEA_WP
src/plugins/wp/wpPropId.ml: CEA_WP
......
......@@ -34,9 +34,6 @@ ifneq ("$(FRAMAC_INTERNAL)","yes")
include $(FRAMAC_SHARE)/Makefile.config
endif
# Why3 API Available
WHY3API=@WHY3API@
# Coq Resources Installation
include $(PLUGIN_DIR)/share/Makefile.resources
......@@ -121,7 +118,6 @@ PLUGIN_DISTRIB_EXTERNAL:= \
CEA_WP_GENEREATED= script.ml rformat.ml driver.ml
# --------------------------------------------------------------------------
# --- Tests ---
# --------------------------------------------------------------------------
......@@ -149,7 +145,13 @@ else
CONFIG_STATUS_DIR=.
endif
$(Wp_DIR)/Makefile: $(Wp_DIR)/Makefile.in $(Wp_DIR)/share/Makefile.resources $(CONFIG_STATUS_DIR)/config.status
WP_CONFIGURE_MAKEFILE= \
$(Wp_DIR)/Makefile.in \
$(Wp_DIR)/share/Makefile.coqwp \
$(Wp_DIR)/share/Makefile.resources \
$(CONFIG_STATUS_DIR)/config.status
$(Wp_DIR)/Makefile: $(WP_CONFIGURE_MAKEFILE)
@cd $(CONFIG_STATUS_DIR) && ./config.status --file $@
# --------------------------------------------------------------------------
......@@ -226,23 +228,16 @@ clean::
## All relative to share/
WP_COQ_SOURCES= $(addprefix coqwp/, $(COQ_LIBS_CEA) $(COQ_LIBS_INRIA))
WHY3_COQ_SOURCES= $(addprefix why3/, $(COQ_LIBS_CEA))
ALL_COQ_SOURCES= $(WP_COQ_SOURCES) $(WHY3_COQ_SOURCES)
ALL_COQ_SOURCES= $(addprefix coqwp/, $(COQ_LIBS_CEA) $(COQ_LIBS_INRIA))
ALL_COQ_BINARIES= $(addsuffix o, $(ALL_COQ_SOURCES))
ALL_ERGO_SOURCES= $(addprefix ergo/, $(ERGO_LIBS_CEA) $(ERGO_LIBS_INRIA))
ALL_WHY3_SOURCES= $(addprefix why3/frama_c_wp/, $(WHY3_LIBS_CEA))
ALL_WHY3_API_SOURCES= $(addprefix why3/frama_c_wp/, $(WHY3_LIBS_CEA))
ALL_RESOURCES= \
wp.driver \
why3/coq.drv \
why3/why3.conf \
$(ALL_COQ_SOURCES) \
$(ALL_ERGO_SOURCES) \
$(ALL_WHY3_SOURCES) \
$(ALL_WHY3_API_SOURCES)
$(ALL_WHY3_SOURCES)
INSTALL_OPT?=
INSTALL_SHARE=@$(Wp_DIR)/share/instwp $(INSTALL_OPT)
......@@ -260,55 +255,17 @@ $(Wp_DIR)/share/instwp: $(Wp_DIR)/share/install.ml
# --- Pre-Compiled Coq Libraries ---
# --------------------------------------------------------------------------
.PHONY: wp-coq wp-why3 wp-coq-all wp-coq-clean wp-coq-install wp-coq-uninstall
wp-coq-all: wp-coq wp-why3
wp-coq: coqwpcompile
@echo "Run 'make wp-coq-install' to install all precompiled libraries"
wp-why3: why3compile
@echo "Run 'make wp-coq-install' to install all precompiled libraries"
WP_COQC_ENABLED=@COQC@
WP_WHY3COQC_ENABLED=@WHY3COQC@
include $(Wp_DIR)/share/Makefile
wp-coq-install:
$(PRINT_INSTALL) "Coq Libraries"
$(INSTALL_SHARE) -f -p -s \
-i $(Wp_DIR)/share \
-d $(FRAMAC_DATADIR)/wp \
$(ALL_COQ_BINARIES)
ifeq ($(WP_COQC_ENABLED),yes)
wp-coq-uninstall:
$(PRINT_RM) "Coq Libraries"
@rm -f $(FRAMAC_DATADIR)/wp/why3/*.vo
@rm -f $(FRAMAC_DATADIR)/wp/coqwp/*.vo
@rm -f $(FRAMAC_DATADIR)/wp/coqwp/*/*.vo
include $(Wp_DIR)/share/Makefile.coqwp
# --------------------------------------------------------------------------
# --- Why3 configuration
# --------------------------------------------------------------------------
byte:: coqwpcompile
opt:: coqwpcompile
clean:: wp-coq-clean
byte:: $(Wp_DIR)/share/why3/why3.conf
opt:: $(Wp_DIR)/share/why3/why3.conf
$(Wp_DIR)/share/why3/why3.conf: config.status $(Wp_DIR)/Makefile.in
$(PRINT_MAKING) "extra-config for why3"
$(RM) $@
@printf "[prover_modifiers]\n" >> $@
@printf "name=\"Coq\"\n" >> $@
@printf "option=\"-Q $(FRAMAC_DATADIR)/wp/why3 ''\"\n" >> $@
@printf "driver=\"$(FRAMAC_DATADIR)/wp/why3/coq.drv\"\n" >> $@
@printf "\n" >> $@
@printf "[editor_modifiers coqide]\n" >> $@
@printf "option=\"-I $(FRAMAC_DATADIR)/wp/why3\"\n" >> $@
@printf "\n" >> $@
@printf "[editor_modifiers proofgeneral-coq]\n" >> $@
@printf "option=\"--eval \\\\\"(setq coq-load-path (cons '(\\\\\\\\\\\\\"$(FRAMAC_DATADIR)/wp/why3\\\\\\\\\\\\\" \\\\\\\\\\\\\"\\\\\\\\\\\\\") coq-load-path))\\\\\"\"\n" >> $@
$(CHMOD_RO) $@
endif #($(WP_COQC_ENABLED),yes)
# --------------------------------------------------------------------------
# --- Installation ---
......
......@@ -42,13 +42,6 @@ AC_ARG_ENABLE(
WPCOQ=yes
)
AC_ARG_ENABLE(
wp-why3,
[ --enable-wp-why3 Wp precompiled Why3-Coq libraries (default: yes)],
WPWHY3COQ=$enableval,
WPWHY3COQ=yes
)
plugin_require(wp,qed)
plugin_require(wp,rtegen)
plugin_use(wp,gui)
......@@ -105,49 +98,6 @@ if test "$ENABLE_WP" != "no"; then
fi
AC_SUBST(COQC)
## Configuring for WHY3-COQ
if test "$COQC" = "yes" -a "$WPWHY3COQ" = "yes" ; then
AC_CHECK_PROG(WHY3COQC,why3,yes,no)
if test "$WHY3COQC" = "yes" ; then
WHY3VERSION=`why3 --version | sed -n -e 's|.*version *\([[^ ]]*\)$|\1|p' `
case $WHY3VERSION in
1.*)
AC_MSG_RESULT(why3 version $WHY3VERSION found)
WHY3LIB=`why3 --print-libdir`
if test -f $WHY3LIB/coq/BuiltIn.vo ; then
AC_MSG_RESULT(why3 compiled coq libraries found)
else
AC_MSG_RESULT(why3 compiled coq libraries not found in $WHY3LIB)
WHY3COQC="no"
fi
;;
*)
AC_MSG_RESULT(why3 unsupported version $WHY3VERSION)
WHY3COQC="no"
;;
esac
else
AC_MSG_NOTICE(rerun configure to make wp using why3 (1.0.0+))
fi
else
WHY3COQC="no"
fi
AC_SUBST(WHY3COQC)
## Configuring for WHY3-API
WHY3API_VERSION=$($OCAMLFIND query why3 -format %v)
case $WHY3API_VERSION in
1.*)
AC_MSG_RESULT(why3 api $WHY3API_VERSION found)
WHY3API="yes"
;;
*)
AC_MSG_RESULT(why3 api not found (no why3 prover detection))
WHY3API="no"
;;
esac
AC_SUBST(WHY3API)
fi
write_plugin_config(Makefile)
......@@ -21,69 +21,18 @@
##########################################################################
WPLSHARE=$(Wp_DIR)/share
# --------------------------------------------------------------------------
# --- Coq Compilation
# --------------------------------------------------------------------------
.PHONY: all why3compile coqwpcompile clean depend wp-coq-clean
WPLSHARE=$(Wp_DIR)/share
wp-coq-clean:
find $(Wp_DIR) \( -name "*.vo" -or -name "*.glob" \) -print -delete
rm -f $(WPLSHARE)/coqwp/.depend $(WPLSHARE)/why3/.depend
clean:: wp-coq-clean
clean:: wp-coq-clean
#########################
## For why3 directory ##
ifeq ($(WP_WHY3COQC_ENABLED),yes)
byte:: why3compile
opt:: why3compile
why3compile: $(addprefix $(WPLSHARE)/why3/, $(addsuffix o, $(COQ_LIBS_CEA)))
WHY3LIB:=$(shell why3 --print-libdir)
WHY3INCLUDES= -R $(WHY3LIB)/coq Why3 -R $(WPLSHARE)/why3 ''
$(WPLSHARE)/why3/%.vo: $(WPLSHARE)/why3/%.v
echo "Coqc $@"
echo coqc -w none $(WHY3INCLUDES) $<
coqc -w none $(WHY3INCLUDES) $<
$(WPLSHARE)/why3/%.ide: $(WPLSHARE)/why3/%.v
echo "Coqide $@"
@coqide $(WHY3INCLUDES) $<
$(WPLSHARE)/why3/.depend: $(addprefix $(WPLSHARE)/, $(WHY3_COQ_SOURCES))
echo "Coqdep for $(WPLSHARE)/why3"
@coqdep $(WHY3INCLUDES) $(WPLSHARE)/why3/*.v $(WPLSHARE)/why3/**/*.v > $@
ifneq ($(MAKECMDGOALS),clean)
ifneq ($(MAKECMDGOALS),distclean)
ifneq ($(MAKECMDGOALS),smartclean)
sinclude $(WPLSHARE)/why3/.depend
endif
endif
endif
endif # ($(WP_WHY3COQC_ENABLED),yes)
#########################
## For coqwp directory ##
ifeq ($(WP_COQC_ENABLED),yes)
byte:: coqwpcompile
opt:: coqwpcompile
coqwpcompile: $(addprefix $(WPLSHARE)/coqwp/, $(addsuffix o, $(COQ_LIBS_CEA) $(COQ_LIBS_INRIA)))
.PHONY: coqwpcompile
COQWPINCLUDES= -R $(WPLSHARE)/coqwp ''
COQWPBINARIES= $(addprefix $(WPLSHARE)/, $(ALL_COQ_BINARIES))
coqwpcompile: $(COQWPBINARIES)
$(WPLSHARE)/coqwp/%.vo: $(WPLSHARE)/coqwp/%.v
echo "Coqc $<"
......@@ -94,9 +43,39 @@ $(WPLSHARE)/coqwp/%.ide: $(WPLSHARE)/coqwp/%.v
coqide $(COQWPINCLUDES) $<
$(WPLSHARE)/coqwp/.depend: $(addprefix $(WPLSHARE)/, $(WP_COQ_SOURCES))
echo "Coqdep for $(WPLSHARE)/coqwp"
echo "Coqdep $(WPLSHARE)/coqwp"
@coqdep $(COQWPINCLUDES) $(WPLSHARE)/coqwp/*.v $(WPLSHARE)/coqwp/**/*.v > $@
# --------------------------------------------------------------------------
# --- Additional Targets
# --------------------------------------------------------------------------
.PHONY: wp-coq-compile wp-coq-clean wp-coq-install wp-coq-uninstall
wp-coq-compile: coqwpcompile
@echo "Run 'make wp-coq-install' to install all precompiled libraries"
wp-coq-clean:
find $(Wp_DIR) \( -name "*.vo" -or -name "*.glob" -or -name ".*.aux" \) -delete
rm -f $(WPLSHARE)/coqwp/.depend
wp-coq-install:
$(PRINT_INSTALL) "Coq Libraries"
$(INSTALL_SHARE) -f -p -s \
-i $(Wp_DIR)/share \
-d $(FRAMAC_DATADIR)/wp \
$(ALL_COQ_BINARIES)
wp-coq-uninstall:
$(PRINT_RM) "Coq Libraries"
@rm -f $(FRAMAC_DATADIR)/wp/why3/*.vo
@rm -f $(FRAMAC_DATADIR)/wp/coqwp/*.vo
@rm -f $(FRAMAC_DATADIR)/wp/coqwp/*/*.vo
# --------------------------------------------------------------------------
# --- Coq Dependencies
# --------------------------------------------------------------------------
ifneq ($(MAKECMDGOALS),clean)
ifneq ($(MAKECMDGOALS),distclean)
ifneq ($(MAKECMDGOALS),smartclean)
......@@ -105,11 +84,4 @@ endif
endif
endif
endif #($(WP_COQC_ENABLED),yes)
# End of file
##########################################################################
# Local Variables:
# mode: makefile
# End:
# --------------------------------------------------------------------------
##########################################################################
# #
# This file is part of WP plug-in of Frama-C. #
# #
# Copyright (C) 2007-2019 #
# CEA (Commissariat a l'energie atomique et aux energies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
#not distributed
include Makefile.resources
HEADERS=../../../../headers
LGPL_HEADERS=../../../../headers/open-source
HEADACHE ?= headache -c $(HEADERS)/headache_config.txt
headers:
$(HEADACHE) -h $(LGPL_HEADERS)/CEA_WP $(ALL_CEA_RESOURCES)
$(HEADACHE) -h $(LGPL_HEADERS)/MODIFIED_WHY3 $(ALL_MODIFIED_WHY3_RESOURCES)
$(HEADACHE) -h $(LGPL_HEADERS)/UNMODIFIED_WHY3 $(ALL_UNMODIFIED_WHY3_RESOURCES)
# target used by developers of wp/share directory
.PHONY: headers.wp_share_src
headers.wp_share_src:
$(HEADACHE) -h $(LGPL_HEADERS)/CEA_WP $(WP_SHARE_SRC_CEA_RESOURCES)
$(HEADACHE) -h $(LGPL_HEADERS)/MODIFIED_WHY3 $(ALL_MODIFIED_WHY3_RESOURCES)
$(HEADACHE) -h $(LGPL_HEADERS)/UNMODIFIED_WHY3 $(ALL_UNMODIFIED_WHY3_RESOURCES)
##########################################################################
# Local Variables:
# mode: makefile
# End:
......@@ -24,8 +24,6 @@
# --- Why-3 Libraries
# --------------------------------------------------------------------------
# See also COQ_LIBS_CEA
## Used in share/why3
WHY3_LIBS_CEA:= \
......@@ -46,7 +44,8 @@ WHY3_API_LIBS_CEA:= WHY3_LIBS_CEA
# --- Coq Libraries
# --------------------------------------------------------------------------
## Used in share/coqwp and share/why3
## Used in share/coqwp
COQ_LIBS_CEA:= \
ArcTrigo.v \
Bits.v \
......@@ -63,7 +62,6 @@ COQ_LIBS_CEA:= \
Vlist.v \
Zbits.v
## Used in share/coqwp only
COQ_LIBS_INRIA:=\
BuiltIn.v \
HighOrd.v \
......@@ -71,6 +69,7 @@ COQ_LIBS_INRIA:=\
int/Abs.v \
int/ComputerDivision.v \
int/EuclideanDivision.v \
int/ComputerOfEuclideanDivision.v \
int/Exponentiation.v \
int/Int.v \
int/MinMax.v \
......@@ -85,14 +84,14 @@ COQ_LIBS_INRIA:=\
real/Square.v \
real/ExpLog.v \
real/PowerReal.v \
real/Trigonometry.v \
for_drivers/ComputerOfEuclideanDivision.v
real/Trigonometry.v
# --------------------------------------------------------------------------
# --- Alt-Ergo Libraries
# --------------------------------------------------------------------------
# Used in share/ergo
ERGO_LIBS_CEA:= \
ArcTrigo.mlw \
Cbits.mlw \
......@@ -106,11 +105,11 @@ ERGO_LIBS_CEA:= \
Vset.mlw \
Vlist.mlw
# Used in share/ergo
ERGO_LIBS_INRIA:= \
bool.Bool.mlw \
int.Abs.mlw \
int.ComputerDivision.mlw \
int.ComputerOfEuclideanDivision.mlw \
int.Int.mlw \
int.MinMax.mlw \
map.Map.mlw \
......@@ -138,7 +137,6 @@ WP_SHARE_SRC_CEA_RESOURCES:= \
wp.driver \
why3/coq.drv \
$(addprefix why3/frama_c_wp/, $(WHY3_LIBS_CEA)) \
$(addprefix why3/, $(COQ_LIBS_CEA)) \
$(addprefix coqwp/, $(COQ_LIBS_CEA)) \
$(addprefix ergo/, $(ERGO_LIBS_CEA))
......
......@@ -30,10 +30,10 @@ Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require int.ComputerDivision.
Require int.ComputerOfEuclideanDivision.
Require real.Real.
Require real.RealInfix.
Require real.FromInt.
Require for_drivers.ComputerOfEuclideanDivision.
Require Cint.
(* Why3 goal *)
......
......@@ -29,10 +29,10 @@ Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require int.ComputerDivision.
Require int.ComputerOfEuclideanDivision.
Require real.Real.
Require real.RealInfix.
Require real.FromInt.
Require for_drivers.ComputerOfEuclideanDivision.
(* Why3 goal *)
Definition match_bool {a:Type} {a_WT:WhyType a} : bool -> a -> a -> a.
......
(**************************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2019 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
(* énergies alternatives). *)
(* *)
(**************************************************************************)
(* this is the prelude for Alt-Ergo, version >= 0.95.2 *)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
......
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Reals.R_sqrt.
Require Reals.Rbasic_fun.
Require Reals.Rtrigo_def.
Require Reals.Rtrigo1.
Require Reals.Ratan.
Require BuiltIn.
Require real.Real.
Require real.RealInfix.
Require real.Abs.
Require real.Square.
Require real.Trigonometry.
(* Why3 goal *)
Definition asin : R -> R.
Admitted.
(* Why3 goal *)
Definition acos : R -> R.
Admitted.
(* Why3 goal *)
Lemma Sin_asin :
forall (x:R), (((-1%R)%R <= x)%R /\ (x <= 1%R)%R) ->
((Reals.Rtrigo_def.sin (asin x)) = x).
Admitted.
(* Why3 goal *)
Lemma Cos_acos :
forall (x:R), (((-1%R)%R <= x)%R /\ (x <= 1%R)%R) ->
((Reals.Rtrigo_def.cos (acos x)) = x).
Admitted.
This diff is collapsed.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require real.Real.
Require real.RealInfix.
Require Import RIneq.
(* Why3 goal *)
Lemma abs_def :
forall (x:Z),
((0%Z <= x)%Z -> ((ZArith.BinInt.Z.abs x) = x)) /\
(~ (0%Z <= x)%Z -> ((ZArith.BinInt.Z.abs x) = (-x)%Z)).
Proof.
exact int.Abs.abs_def.
Qed.
##########################################################################
# #
# This file is part of WP plug-in of Frama-C. #
# #
# Copyright (C) 2007-2019 #
# CEA (Commissariat a l'energie atomique et aux energies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #