From owner-svn-ports-head@FreeBSD.ORG Sun Mar 22 18:39:35 2015 Return-Path: Delivered-To: svn-ports-head@freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) (using TLSv1.2 with cipher AECDH-AES256-SHA (256/256 bits)) (No client certificate requested) by hub.freebsd.org (Postfix) with ESMTPS id 27CDF179; Sun, 22 Mar 2015 18:39:35 +0000 (UTC) Received: from svn.freebsd.org (svn.freebsd.org [IPv6:2001:1900:2254:2068::e6a:0]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mx1.freebsd.org (Postfix) with ESMTPS id 123AA278; Sun, 22 Mar 2015 18:39:35 +0000 (UTC) Received: from svn.freebsd.org ([127.0.1.70]) by svn.freebsd.org (8.14.9/8.14.9) with ESMTP id t2MIdZ18044113; Sun, 22 Mar 2015 18:39:35 GMT (envelope-from marino@FreeBSD.org) Received: (from marino@localhost) by svn.freebsd.org (8.14.9/8.14.9/Submit) id t2MIdYNo044110; Sun, 22 Mar 2015 18:39:34 GMT (envelope-from marino@FreeBSD.org) Message-Id: <201503221839.t2MIdYNo044110@svn.freebsd.org> X-Authentication-Warning: svn.freebsd.org: marino set sender to marino@FreeBSD.org using -f From: John Marino Date: Sun, 22 Mar 2015 18:39:34 +0000 (UTC) To: ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org Subject: svn commit: r381945 - in head/devel/frama-c: . files X-SVN-Group: ports-head MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-BeenThere: svn-ports-head@freebsd.org X-Mailman-Version: 2.1.18-1 Precedence: list List-Id: SVN commit messages for the ports tree for head List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 22 Mar 2015 18:39:35 -0000 Author: marino Date: Sun Mar 22 18:39:33 2015 New Revision: 381945 URL: https://svnweb.freebsd.org/changeset/ports/381945 QAT: https://qat.redports.org/buildarchive/r381945/ Log: devel/frama-c: upgrade version 20140301 => 20150201 (Unbreak) The big change is the removal of options. With Sodium, the gui, plugins, coq and why3 are all enabled by default. The pain to disable these options isn't worth the hassle of maintaining the plist with all its possible variations. Notes: - The distfile can only be extracted by gtar. - Reset maintainership - This ports is extremely sensitive to Ocamlgraph changes. Ocamlgraph should not be updated without checking breakage on frama-c first - used @dir instead of .keepme - Made some tabbing changes Deleted: head/devel/frama-c/files/ Modified: head/devel/frama-c/Makefile head/devel/frama-c/distinfo head/devel/frama-c/pkg-plist Modified: head/devel/frama-c/Makefile ============================================================================== --- head/devel/frama-c/Makefile Sun Mar 22 18:16:41 2015 (r381944) +++ head/devel/frama-c/Makefile Sun Mar 22 18:39:33 2015 (r381945) @@ -1,80 +1,31 @@ # Created by: b.f. # $FreeBSD$ -PORTNAME= frama-c -DISTVERSIONPREFIX= Neon- -DISTVERSION= 20140301 -PORTREVISION= 2 -CATEGORIES= devel -MASTER_SITES= http://frama-c.com/download/ LOCAL/bf +PORTNAME= frama-c +DISTVERSIONPREFIX= Sodium- +DISTVERSION= 20150201 +CATEGORIES= devel +MASTER_SITES= http://frama-c.com/download/ -MAINTAINER= bf@FreeBSD.org +MAINTAINER= ports@FreeBSD.org COMMENT= Extensible platform for source-code analysis of C LICENSE= LGPL21 -BROKEN= Fails to build with ocamlgraph 1.8.6 - +EXTRACT_DEPENDS= gtar:${PORTSDIR}/archivers/gtar BUILD_DEPENDS= ${LOCALBASE}/lib/ocaml/ocamlgraph/graph.a:${PORTSDIR}/math/ocaml-ocamlgraph RUN_DEPENDS= ${LOCALBASE}/lib/ocaml/ocamlgraph/graph.a:${PORTSDIR}/math/ocaml-ocamlgraph USES= gmake USE_OCAML= yes GNU_CONFIGURE= yes +EXTRACT_CMD= gtar +EXTRACT_BEFORE_ARGS= -xf CONFIGURE_ARGS+=--with-cpp="${FRAMAC_DEFAULT_CPP}" MAKE_ENV+= FRAMAC_LIBDIR="${PREFIX}/lib/frama-c" -OPTIONS_DEFINE= ALTERGO COQ GUI PLUGINS -OPTIONS_DEFAULT=ALTERGO GUI PLUGINS -OPTIONS_SUB= yes -ALTERGO_DESC= Alt-Ergo plugin (requires PLUGINS) -COQ_DESC= Coq plugin (requires PLUGINS) -GUI_DESC= Graphical User Interface (requires PLUGINS) - -.include - FRAMAC_DEFAULT_CPP?= ${CPP} -C -I${DATADIR}/libc -I. -.if ${PORT_OPTIONS:MALTERGO} -.if !${PORT_OPTIONS:MPLUGINS} -IGNORE= the Alt-Ergo plugin requires the PLUGINS option to be enabled -.endif -BUILD_DEPENDS+= alt-ergo:${PORTSDIR}/math/alt-ergo -RUN_DEPENDS+= alt-ergo:${PORTSDIR}/math/alt-ergo -.else -CONFIGURE_ENV+= HAS_ALTERGO=no -.endif - -.if ${PORT_OPTIONS:MCOQ} -.if !${PORT_OPTIONS:MPLUGINS} -IGNORE= the Coq plugin requires the PLUGINS option to be enabled -.endif -BUILD_DEPENDS+= coqc:${PORTSDIR}/math/coq -RUN_DEPENDS+= coqc:${PORTSDIR}/math/coq -.else -CONFIGURE_ENV+= HAS_COQ=no -.endif - -.if ${PORT_OPTIONS:MGUI} -.if !${PORT_OPTIONS:MPLUGINS} -IGNORE= the GUI requires the PLUGINS option to be enabled -.endif -BUILD_DEPENDS+= lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2 -RUN_DEPENDS+= lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2 -CONFIGURE_ARGS+= --enable-gui -.else -CONFIGURE_ARGS+= --disable-gui -.endif - -.if ${PORT_OPTIONS:MPLUGINS} -BUILD_DEPENDS+= dot:${PORTSDIR}/graphics/graphviz \ - ltl2ba:${PORTSDIR}/math/ltl2ba -RUN_DEPENDS+= dot:${PORTSDIR}/graphics/graphviz \ - ltl2ba:${PORTSDIR}/math/ltl2ba -.else -CONFIGURE_ARGS+= --with-no-plugin -.endif - post-patch: @cd ${WRKSRC}/tests; ${MKDIR} aorai report wp wp_acsl wp_bts \ wp_engine wp_hoare wp_plugin wp_runtime wp_store wp_typed @@ -95,31 +46,6 @@ post-patch: \|$$(CP).*man/|s|$$(CP)|${INSTALL_MAN}|; \ s|$$(CP)|${INSTALL_DATA}|; }' \ ${WRKSRC}/Makefile - @${REINPLACE_CMD} -e 's|HAS_ALTERGO=$$||' \ - -e '\|case $$ALTERGO_VERSION in|{N; s|0\.92\.2|0.94*|;}' \ - -e 's|HAS_COQ=$$||' \ - ${WRKSRC}/configure - @${REINPLACE_CMD} -Ee 's@(\+|/)(lablgtk2)@\1site-lib/\2@' \ - ${WRKSRC}/src/kernel/dynamic.ml - -.if ${PORT_OPTIONS:MGUI} -pre-configure: - @(if [ ! -e ${LOCALBASE}/${OCAML_SITELIBDIR}/lablgtk2/gtkSourceView2.cmi -o \ - ! -e ${LOCALBASE}/${OCAML_SITELIBDIR}/lablgtk2/gnomeCanvas.cmi ] ; then \ - ${ECHO_MSG} "==> The WITH_GUI option for ${PKGNAME} requires" ; \ - ${ECHO_MSG} "==> x11-toolkits/ocaml-lablgtk2 to be built" ; \ - ${ECHO_MSG} "==> WITH_GNOMECANVAS and WITH_GTKSOURCEVIEW2" ; \ - exit 1; fi) - @(if [ ! -e ${LOCALBASE}/lib/ocaml/ocamlgraph/dgraph.cmi ] ; then \ - ${ECHO_MSG} "==> The WITH_GUI option for ${PKGNAME} requires" ; \ - ${ECHO_MSG} "==> math/ocaml-ocamlgraph to be built WITH_GUI" ; \ - exit 1; fi) - -.endif - -post-install: - @${TOUCH} ${STAGEDIR}${PREFIX}/lib/frama-c/plugins/.keep_me \ - ${STAGEDIR}${PREFIX}/lib/frama-c/plugins/gui/.keep_me check regression-test test: build @cd ${WRKSRC}; ${SETENV} ${MAKE_ENV:NCPP=*} \ Modified: head/devel/frama-c/distinfo ============================================================================== --- head/devel/frama-c/distinfo Sun Mar 22 18:16:41 2015 (r381944) +++ head/devel/frama-c/distinfo Sun Mar 22 18:39:33 2015 (r381945) @@ -1,2 +1,2 @@ -SHA256 (frama-c-Neon-20140301.tar.gz) = c5a0606f5c2d56280fd90f979c07ff398acb1e6a661323438b8d0cbd8f9f4731 -SIZE (frama-c-Neon-20140301.tar.gz) = 3122492 +SHA256 (frama-c-Sodium-20150201.tar.gz) = b61638809e5e2f4138052844dd58aa2d2c44d542a65111cc80b65f6b999a4c71 +SIZE (frama-c-Sodium-20150201.tar.gz) = 5993348 Modified: head/devel/frama-c/pkg-plist ============================================================================== --- head/devel/frama-c/pkg-plist Sun Mar 22 18:16:41 2015 (r381944) +++ head/devel/frama-c/pkg-plist Sun Mar 22 18:39:33 2015 (r381945) @@ -1,11 +1,13 @@ bin/frama-c -%%GUI%%bin/frama-c-gui -%%GUI%%bin/frama-c-gui.byte +bin/frama-c-config +bin/frama-c-gui +bin/frama-c-gui.byte bin/frama-c.byte bin/ptests.opt -%%PLUGINS%%lib/frama-c/Constant_Propagation.cmo -%%PLUGINS%%lib/frama-c/Constant_Propagation.cmx -%%PLUGINS%%lib/frama-c/Constant_Propagation.o +lib/frama-c/Constant_Propagation.cmi +lib/frama-c/Constant_Propagation.cmo +lib/frama-c/Constant_Propagation.cmx +lib/frama-c/Constant_Propagation.o lib/frama-c/FCHashtbl.cmi lib/frama-c/FCHashtbl.cmo lib/frama-c/FCHashtbl.cmx @@ -18,51 +20,66 @@ lib/frama-c/FCSet.cmi lib/frama-c/FCSet.cmo lib/frama-c/FCSet.cmx lib/frama-c/FCSet.o -%%PLUGINS%%lib/frama-c/From.cmo -%%PLUGINS%%lib/frama-c/From.cmx -%%PLUGINS%%lib/frama-c/From.o -%%PLUGINS%%lib/frama-c/Impact.cmo -%%PLUGINS%%lib/frama-c/Impact.cmx -%%PLUGINS%%lib/frama-c/Impact.o -%%PLUGINS%%lib/frama-c/Inout.cmo -%%PLUGINS%%lib/frama-c/Inout.cmx -%%PLUGINS%%lib/frama-c/Inout.o -%%PLUGINS%%lib/frama-c/Metrics.cmo -%%PLUGINS%%lib/frama-c/Metrics.cmx -%%PLUGINS%%lib/frama-c/Metrics.o -%%PLUGINS%%lib/frama-c/Occurrence.cmo -%%PLUGINS%%lib/frama-c/Occurrence.cmx -%%PLUGINS%%lib/frama-c/Occurrence.o -%%PLUGINS%%lib/frama-c/Pdg.cmo -%%PLUGINS%%lib/frama-c/Pdg.cmx -%%PLUGINS%%lib/frama-c/Pdg.o -%%PLUGINS%%lib/frama-c/Postdominators.cmo -%%PLUGINS%%lib/frama-c/Postdominators.cmx -%%PLUGINS%%lib/frama-c/Postdominators.o -%%PLUGINS%%lib/frama-c/RteGen.cmo -%%PLUGINS%%lib/frama-c/RteGen.cmx -%%PLUGINS%%lib/frama-c/RteGen.o -%%PLUGINS%%lib/frama-c/Scope.cmo -%%PLUGINS%%lib/frama-c/Scope.cmx -%%PLUGINS%%lib/frama-c/Scope.o -%%PLUGINS%%lib/frama-c/Semantic_callgraph.cmo -%%PLUGINS%%lib/frama-c/Semantic_callgraph.cmx -%%PLUGINS%%lib/frama-c/Semantic_callgraph.o -%%PLUGINS%%lib/frama-c/Slicing.cmo -%%PLUGINS%%lib/frama-c/Slicing.cmx -%%PLUGINS%%lib/frama-c/Slicing.o -%%PLUGINS%%lib/frama-c/Sparecode.cmo -%%PLUGINS%%lib/frama-c/Sparecode.cmx -%%PLUGINS%%lib/frama-c/Sparecode.o -%%PLUGINS%%lib/frama-c/Syntactic_callgraph.cmo -%%PLUGINS%%lib/frama-c/Syntactic_callgraph.cmx -%%PLUGINS%%lib/frama-c/Syntactic_callgraph.o -%%PLUGINS%%lib/frama-c/Users.cmo -%%PLUGINS%%lib/frama-c/Users.cmx -%%PLUGINS%%lib/frama-c/Users.o -%%PLUGINS%%lib/frama-c/Value.cmo -%%PLUGINS%%lib/frama-c/Value.cmx -%%PLUGINS%%lib/frama-c/Value.o +lib/frama-c/From.cmi +lib/frama-c/From.cmo +lib/frama-c/From.cmx +lib/frama-c/From.o +lib/frama-c/Impact.cmi +lib/frama-c/Impact.cmo +lib/frama-c/Impact.cmx +lib/frama-c/Impact.o +lib/frama-c/Inout.cmi +lib/frama-c/Inout.cmo +lib/frama-c/Inout.cmx +lib/frama-c/Inout.o +lib/frama-c/Metrics.cmi +lib/frama-c/Metrics.cmo +lib/frama-c/Metrics.cmx +lib/frama-c/Metrics.o +lib/frama-c/Occurrence.cmi +lib/frama-c/Occurrence.cmo +lib/frama-c/Occurrence.cmx +lib/frama-c/Occurrence.o +lib/frama-c/Pdg.cmi +lib/frama-c/Pdg.cmo +lib/frama-c/Pdg.cmx +lib/frama-c/Pdg.o +lib/frama-c/Postdominators.cmi +lib/frama-c/Postdominators.cmo +lib/frama-c/Postdominators.cmx +lib/frama-c/Postdominators.o +lib/frama-c/RteGen.cmi +lib/frama-c/RteGen.cmo +lib/frama-c/RteGen.cmx +lib/frama-c/RteGen.o +lib/frama-c/Scope.cmi +lib/frama-c/Scope.cmo +lib/frama-c/Scope.cmx +lib/frama-c/Scope.o +lib/frama-c/Semantic_callgraph.cmi +lib/frama-c/Semantic_callgraph.cmo +lib/frama-c/Semantic_callgraph.cmx +lib/frama-c/Semantic_callgraph.o +lib/frama-c/Slicing.cmi +lib/frama-c/Slicing.cmo +lib/frama-c/Slicing.cmx +lib/frama-c/Slicing.o +lib/frama-c/Sparecode.cmi +lib/frama-c/Sparecode.cmo +lib/frama-c/Sparecode.cmx +lib/frama-c/Sparecode.o +lib/frama-c/Syntactic_callgraph.cmi +lib/frama-c/Syntactic_callgraph.cmo +lib/frama-c/Syntactic_callgraph.cmx +lib/frama-c/Syntactic_callgraph.o +lib/frama-c/Users.cmi +lib/frama-c/Users.cmo +lib/frama-c/Users.cmx +lib/frama-c/Users.o +lib/frama-c/Value.cmi +lib/frama-c/Value.cmo +lib/frama-c/Value.cmx +lib/frama-c/Value.o lib/frama-c/abstract_interp.cmi lib/frama-c/abstract_interp.cmo lib/frama-c/abstract_interp.cmx @@ -79,10 +96,10 @@ lib/frama-c/alpha.cmi lib/frama-c/alpha.cmo lib/frama-c/alpha.cmx lib/frama-c/alpha.o -%%GUI%%lib/frama-c/analyses_manager.cmi -%%GUI%%lib/frama-c/analyses_manager.cmo -%%GUI%%lib/frama-c/analyses_manager.cmx -%%GUI%%lib/frama-c/analyses_manager.o +lib/frama-c/analyses_manager.cmi +lib/frama-c/analyses_manager.cmo +lib/frama-c/analyses_manager.cmx +lib/frama-c/analyses_manager.o lib/frama-c/annotations.cmi lib/frama-c/annotations.cmo lib/frama-c/annotations.cmx @@ -95,10 +112,6 @@ lib/frama-c/ast_info.cmi lib/frama-c/ast_info.cmo lib/frama-c/ast_info.cmx lib/frama-c/ast_info.o -lib/frama-c/availexpslv.cmi -lib/frama-c/availexpslv.cmo -lib/frama-c/availexpslv.cmx -lib/frama-c/availexpslv.o lib/frama-c/bag.cmi lib/frama-c/bag.cmo lib/frama-c/bag.cmx @@ -119,18 +132,14 @@ lib/frama-c/bitvector.cmi lib/frama-c/bitvector.cmo lib/frama-c/bitvector.cmx lib/frama-c/bitvector.o -%%GUI%%lib/frama-c/book_manager.cmi -%%GUI%%lib/frama-c/book_manager.cmo -%%GUI%%lib/frama-c/book_manager.cmx -%%GUI%%lib/frama-c/book_manager.o +lib/frama-c/book_manager.cmi +lib/frama-c/book_manager.cmo +lib/frama-c/book_manager.cmx +lib/frama-c/book_manager.o lib/frama-c/boot.cmi lib/frama-c/boot.cmo lib/frama-c/boot.cmx lib/frama-c/boot.o -lib/frama-c/buckx.cmi -lib/frama-c/buckx.cmo -lib/frama-c/buckx.cmx -lib/frama-c/buckx.o lib/frama-c/buckx_c.o lib/frama-c/cabs.cmi lib/frama-c/cabs.cmo @@ -144,14 +153,6 @@ lib/frama-c/cabs_debug.cmi lib/frama-c/cabs_debug.cmo lib/frama-c/cabs_debug.cmx lib/frama-c/cabs_debug.o -lib/frama-c/cabsbranches.cmi -lib/frama-c/cabsbranches.cmo -lib/frama-c/cabsbranches.cmx -lib/frama-c/cabsbranches.o -lib/frama-c/cabscond.cmi -lib/frama-c/cabscond.cmo -lib/frama-c/cabscond.cmx -lib/frama-c/cabscond.o lib/frama-c/cabshelper.cmi lib/frama-c/cabshelper.cmo lib/frama-c/cabshelper.cmx @@ -209,6 +210,10 @@ lib/frama-c/clexer.cmi lib/frama-c/clexer.cmo lib/frama-c/clexer.cmx lib/frama-c/clexer.o +lib/frama-c/clone.cmi +lib/frama-c/clone.cmo +lib/frama-c/clone.cmx +lib/frama-c/clone.o lib/frama-c/cmdline.cmi lib/frama-c/cmdline.cmo lib/frama-c/cmdline.cmx @@ -253,14 +258,10 @@ lib/frama-c/db.cmi lib/frama-c/db.cmo lib/frama-c/db.cmx lib/frama-c/db.o -lib/frama-c/deadcodeelim.cmi -lib/frama-c/deadcodeelim.cmo -lib/frama-c/deadcodeelim.cmx -lib/frama-c/deadcodeelim.o -%%GUI%%lib/frama-c/debug_manager.cmi -%%GUI%%lib/frama-c/debug_manager.cmo -%%GUI%%lib/frama-c/debug_manager.cmx -%%GUI%%lib/frama-c/debug_manager.o +lib/frama-c/debug_manager.cmi +lib/frama-c/debug_manager.cmo +lib/frama-c/debug_manager.cmx +lib/frama-c/debug_manager.o lib/frama-c/descr.cmi lib/frama-c/descr.cmo lib/frama-c/descr.cmx @@ -269,10 +270,11 @@ lib/frama-c/description.cmi lib/frama-c/description.cmo lib/frama-c/description.cmx lib/frama-c/description.o -%%GUI%%lib/frama-c/design.cmi -%%GUI%%lib/frama-c/design.cmo -%%GUI%%lib/frama-c/design.cmx -%%GUI%%lib/frama-c/design.o +lib/frama-c/design.cmi +lib/frama-c/design.cmo +lib/frama-c/design.cmx +lib/frama-c/design.o +lib/frama-c/dgraph.cmi lib/frama-c/dominators.cmi lib/frama-c/dominators.cmo lib/frama-c/dominators.cmx @@ -297,10 +299,10 @@ lib/frama-c/escape.cmi lib/frama-c/escape.cmo lib/frama-c/escape.cmx lib/frama-c/escape.o -lib/frama-c/expcompare.cmi -lib/frama-c/expcompare.cmo -lib/frama-c/expcompare.cmx -lib/frama-c/expcompare.o +lib/frama-c/exn_flow.cmi +lib/frama-c/exn_flow.cmo +lib/frama-c/exn_flow.cmx +lib/frama-c/exn_flow.o lib/frama-c/extlib.cmi lib/frama-c/extlib.cmo lib/frama-c/extlib.cmx @@ -309,18 +311,18 @@ lib/frama-c/file.cmi lib/frama-c/file.cmo lib/frama-c/file.cmx lib/frama-c/file.o -%%GUI%%lib/frama-c/file_manager.cmi -%%GUI%%lib/frama-c/file_manager.cmo -%%GUI%%lib/frama-c/file_manager.cmx -%%GUI%%lib/frama-c/file_manager.o +lib/frama-c/file_manager.cmi +lib/frama-c/file_manager.cmo +lib/frama-c/file_manager.cmx +lib/frama-c/file_manager.o lib/frama-c/filepath.cmi lib/frama-c/filepath.cmo lib/frama-c/filepath.cmx lib/frama-c/filepath.o -%%GUI%%lib/frama-c/filetree.cmi -%%GUI%%lib/frama-c/filetree.cmo -%%GUI%%lib/frama-c/filetree.cmx -%%GUI%%lib/frama-c/filetree.o +lib/frama-c/filetree.cmi +lib/frama-c/filetree.cmo +lib/frama-c/filetree.cmx +lib/frama-c/filetree.o lib/frama-c/filter.cmi lib/frama-c/filter.cmo lib/frama-c/filter.cmx @@ -329,6 +331,11 @@ lib/frama-c/floating_point.cmi lib/frama-c/floating_point.cmo lib/frama-c/floating_point.cmx lib/frama-c/floating_point.o +lib/frama-c/frama_c_config.cmi +lib/frama-c/frama_c_init.cmi +lib/frama-c/frama_c_init.cmo +lib/frama-c/frama_c_init.cmx +lib/frama-c/frama_c_init.o lib/frama-c/frontc.cmi lib/frama-c/frontc.cmo lib/frama-c/frontc.cmx @@ -341,27 +348,31 @@ lib/frama-c/globals.cmi lib/frama-c/globals.cmo lib/frama-c/globals.cmx lib/frama-c/globals.o -%%GUI%%lib/frama-c/gtk_form.cmi -%%GUI%%lib/frama-c/gtk_form.cmo -%%GUI%%lib/frama-c/gtk_form.cmx -%%GUI%%lib/frama-c/gtk_form.o -%%GUI%%lib/frama-c/gtk_helper.cmi -%%GUI%%lib/frama-c/gtk_helper.cmo -%%GUI%%lib/frama-c/gtk_helper.cmx -%%GUI%%lib/frama-c/gtk_helper.o -%%GUI%%lib/frama-c/gui_init.cmi -%%GUI%%lib/frama-c/gui_parameters.cmi -%%GUI%%lib/frama-c/gui_parameters.cmo -%%GUI%%lib/frama-c/gui_parameters.cmx -%%GUI%%lib/frama-c/gui_parameters.o -%%GUI%%lib/frama-c/help_manager.cmi -%%GUI%%lib/frama-c/help_manager.cmo -%%GUI%%lib/frama-c/help_manager.cmx -%%GUI%%lib/frama-c/help_manager.o -%%GUI%%lib/frama-c/history.cmi -%%GUI%%lib/frama-c/history.cmo -%%GUI%%lib/frama-c/history.cmx -%%GUI%%lib/frama-c/history.o +lib/frama-c/graph.cmi +lib/frama-c/graph.cmo +lib/frama-c/graph.cmx +lib/frama-c/graph.o +lib/frama-c/gtk_form.cmi +lib/frama-c/gtk_form.cmo +lib/frama-c/gtk_form.cmx +lib/frama-c/gtk_form.o +lib/frama-c/gtk_helper.cmi +lib/frama-c/gtk_helper.cmo +lib/frama-c/gtk_helper.cmx +lib/frama-c/gtk_helper.o +lib/frama-c/gui_init.cmi +lib/frama-c/gui_parameters.cmi +lib/frama-c/gui_parameters.cmo +lib/frama-c/gui_parameters.cmx +lib/frama-c/gui_parameters.o +lib/frama-c/help_manager.cmi +lib/frama-c/help_manager.cmo +lib/frama-c/help_manager.cmx +lib/frama-c/help_manager.o +lib/frama-c/history.cmi +lib/frama-c/history.cmo +lib/frama-c/history.cmx +lib/frama-c/history.o lib/frama-c/hook.cmi lib/frama-c/hook.cmo lib/frama-c/hook.cmx @@ -390,14 +401,11 @@ lib/frama-c/int_Base.cmi lib/frama-c/int_Base.cmo lib/frama-c/int_Base.cmx lib/frama-c/int_Base.o -lib/frama-c/int_Interv.cmi -lib/frama-c/int_Interv.cmo -lib/frama-c/int_Interv.cmx -lib/frama-c/int_Interv.o -lib/frama-c/int_Interv_Map.cmi -lib/frama-c/int_Interv_Map.cmo -lib/frama-c/int_Interv_Map.cmx -lib/frama-c/int_Interv_Map.o +lib/frama-c/int_Intervals.cmi +lib/frama-c/int_Intervals.cmo +lib/frama-c/int_Intervals.cmx +lib/frama-c/int_Intervals.o +lib/frama-c/int_Intervals_sig.cmi lib/frama-c/integer.cmi lib/frama-c/integer.cmo lib/frama-c/integer.cmx @@ -418,23 +426,15 @@ lib/frama-c/kernel_function.cmi lib/frama-c/kernel_function.cmo lib/frama-c/kernel_function.cmx lib/frama-c/kernel_function.o -lib/frama-c/lattice_Interval_Set.cmi -lib/frama-c/lattice_Interval_Set.cmo -lib/frama-c/lattice_Interval_Set.cmx -lib/frama-c/lattice_Interval_Set.o lib/frama-c/lattice_type.cmi -%%GUI%%lib/frama-c/launcher.cmi -%%GUI%%lib/frama-c/launcher.cmo -%%GUI%%lib/frama-c/launcher.cmx -%%GUI%%lib/frama-c/launcher.o +lib/frama-c/launcher.cmi +lib/frama-c/launcher.cmo +lib/frama-c/launcher.cmx +lib/frama-c/launcher.o lib/frama-c/lexerhack.cmi lib/frama-c/lexerhack.cmo lib/frama-c/lexerhack.cmx lib/frama-c/lexerhack.o -lib/frama-c/liveness.cmi -lib/frama-c/liveness.cmo -lib/frama-c/liveness.cmx -lib/frama-c/liveness.o lib/frama-c/lmap.cmi lib/frama-c/lmap.cmo lib/frama-c/lmap.cmx @@ -497,30 +497,18 @@ lib/frama-c/loop.cmi lib/frama-c/loop.cmo lib/frama-c/loop.cmx lib/frama-c/loop.o -lib/frama-c/machdep_ppc_32.cmi -lib/frama-c/machdep_ppc_32.cmo -lib/frama-c/machdep_ppc_32.cmx -lib/frama-c/machdep_ppc_32.o -lib/frama-c/machdep_x86_16.cmi -lib/frama-c/machdep_x86_16.cmo -lib/frama-c/machdep_x86_16.cmx -lib/frama-c/machdep_x86_16.o -lib/frama-c/machdep_x86_32.cmi -lib/frama-c/machdep_x86_32.cmo -lib/frama-c/machdep_x86_32.cmx -lib/frama-c/machdep_x86_32.o -lib/frama-c/machdep_x86_64.cmi -lib/frama-c/machdep_x86_64.cmo -lib/frama-c/machdep_x86_64.cmx -lib/frama-c/machdep_x86_64.o +lib/frama-c/machdeps.cmi +lib/frama-c/machdeps.cmo +lib/frama-c/machdeps.cmx +lib/frama-c/machdeps.o lib/frama-c/map_Lattice.cmi lib/frama-c/map_Lattice.cmo lib/frama-c/map_Lattice.cmx lib/frama-c/map_Lattice.o -%%GUI%%lib/frama-c/menu_manager.cmi -%%GUI%%lib/frama-c/menu_manager.cmo -%%GUI%%lib/frama-c/menu_manager.cmx -%%GUI%%lib/frama-c/menu_manager.o +lib/frama-c/menu_manager.cmi +lib/frama-c/menu_manager.cmo +lib/frama-c/menu_manager.cmx +lib/frama-c/menu_manager.o lib/frama-c/mergecil.cmi lib/frama-c/mergecil.cmo lib/frama-c/mergecil.cmx @@ -533,10 +521,7 @@ lib/frama-c/offsetmap.cmi lib/frama-c/offsetmap.cmo lib/frama-c/offsetmap.cmx lib/frama-c/offsetmap.o -lib/frama-c/offsetmap_bitwise.cmi -lib/frama-c/offsetmap_bitwise.cmo -lib/frama-c/offsetmap_bitwise.cmx -lib/frama-c/offsetmap_bitwise.o +lib/frama-c/offsetmap_bitwise_sig.cmi lib/frama-c/offsetmap_lattice_with_isotropy.cmi lib/frama-c/offsetmap_sig.cmi lib/frama-c/oneret.cmi @@ -555,6 +540,10 @@ lib/frama-c/parameter_builder.cmi lib/frama-c/parameter_builder.cmo lib/frama-c/parameter_builder.cmx lib/frama-c/parameter_builder.o +lib/frama-c/parameter_category.cmi +lib/frama-c/parameter_category.cmo +lib/frama-c/parameter_category.cmx +lib/frama-c/parameter_category.o lib/frama-c/parameter_customize.cmi lib/frama-c/parameter_customize.cmo lib/frama-c/parameter_customize.cmx @@ -580,33 +569,35 @@ lib/frama-c/plugin.cmi lib/frama-c/plugin.cmo lib/frama-c/plugin.cmx lib/frama-c/plugin.o -lib/frama-c/plugins/.keep_me -%%PLUGINS%%lib/frama-c/plugins/Aorai.cmi -%%PLUGINS%%lib/frama-c/plugins/Aorai.cmo -%%PLUGINS%%lib/frama-c/plugins/Aorai.cmxs -%%PLUGINS%%lib/frama-c/plugins/Obfuscator.cmi -%%PLUGINS%%lib/frama-c/plugins/Obfuscator.cmo -%%PLUGINS%%lib/frama-c/plugins/Obfuscator.cmxs -%%PLUGINS%%lib/frama-c/plugins/Report.cmi -%%PLUGINS%%lib/frama-c/plugins/Report.cmo -%%PLUGINS%%lib/frama-c/plugins/Report.cmxs -%%GUI%%lib/frama-c/plugins/Security_slicing.cmi -%%GUI%%lib/frama-c/plugins/Security_slicing.cmo -%%GUI%%lib/frama-c/plugins/Security_slicing.cmxs -%%PLUGINS%%lib/frama-c/plugins/Wp.cma -%%PLUGINS%%lib/frama-c/plugins/Wp.cmi -%%PLUGINS%%lib/frama-c/plugins/Wp.cmxs -lib/frama-c/plugins/gui/.keep_me -%%GUI%%lib/frama-c/plugins/gui/Security_slicing.cmi -%%GUI%%lib/frama-c/plugins/gui/Security_slicing.cmo -%%GUI%%lib/frama-c/plugins/gui/Security_slicing.cmxs -%%GUI%%lib/frama-c/plugins/gui/Wp.cma -%%GUI%%lib/frama-c/plugins/gui/Wp.cmi -%%GUI%%lib/frama-c/plugins/gui/Wp.cmxs -%%GUI%%lib/frama-c/pretty_source.cmi -%%GUI%%lib/frama-c/pretty_source.cmo -%%GUI%%lib/frama-c/pretty_source.cmx -%%GUI%%lib/frama-c/pretty_source.o +lib/frama-c/plugins/Aorai.cmi +lib/frama-c/plugins/Aorai.cmo +lib/frama-c/plugins/Aorai.cmxs +lib/frama-c/plugins/Obfuscator.cmi +lib/frama-c/plugins/Obfuscator.cmo +lib/frama-c/plugins/Obfuscator.cmxs +lib/frama-c/plugins/Report.cmi +lib/frama-c/plugins/Report.cmo +lib/frama-c/plugins/Report.cmxs +lib/frama-c/plugins/Security_slicing.cmi +lib/frama-c/plugins/Security_slicing.cmo +lib/frama-c/plugins/Security_slicing.cmxs +lib/frama-c/plugins/Wp.cma +lib/frama-c/plugins/Wp.cmi +lib/frama-c/plugins/Wp.cmxs +lib/frama-c/plugins/gui/Security_slicing.cmi +lib/frama-c/plugins/gui/Security_slicing.cmo +lib/frama-c/plugins/gui/Security_slicing.cmxs +lib/frama-c/plugins/gui/Wp.cma +lib/frama-c/plugins/gui/Wp.cmi +lib/frama-c/plugins/gui/Wp.cmxs +lib/frama-c/precise_locs.cmi +lib/frama-c/precise_locs.cmo +lib/frama-c/precise_locs.cmx +lib/frama-c/precise_locs.o +lib/frama-c/pretty_source.cmi +lib/frama-c/pretty_source.cmo +lib/frama-c/pretty_source.cmx +lib/frama-c/pretty_source.o lib/frama-c/pretty_utils.cmi lib/frama-c/pretty_utils.cmo lib/frama-c/pretty_utils.cmx @@ -624,10 +615,10 @@ lib/frama-c/project.cmi lib/frama-c/project.cmo lib/frama-c/project.cmx lib/frama-c/project.o -%%GUI%%lib/frama-c/project_manager.cmi -%%GUI%%lib/frama-c/project_manager.cmo -%%GUI%%lib/frama-c/project_manager.cmx -%%GUI%%lib/frama-c/project_manager.o +lib/frama-c/project_manager.cmi +lib/frama-c/project_manager.cmo +lib/frama-c/project_manager.cmx +lib/frama-c/project_manager.o lib/frama-c/project_skeleton.cmi lib/frama-c/project_skeleton.cmo lib/frama-c/project_skeleton.cmx @@ -636,10 +627,10 @@ lib/frama-c/property.cmi lib/frama-c/property.cmo lib/frama-c/property.cmx lib/frama-c/property.o -%%GUI%%lib/frama-c/property_navigator.cmi -%%GUI%%lib/frama-c/property_navigator.cmo -%%GUI%%lib/frama-c/property_navigator.cmx -%%GUI%%lib/frama-c/property_navigator.o +lib/frama-c/property_navigator.cmi +lib/frama-c/property_navigator.cmo +lib/frama-c/property_navigator.cmx +lib/frama-c/property_navigator.o lib/frama-c/property_status.cmi lib/frama-c/property_status.cmo lib/frama-c/property_status.cmx @@ -655,14 +646,6 @@ lib/frama-c/rangemap.cmi lib/frama-c/rangemap.cmo lib/frama-c/rangemap.cmx lib/frama-c/rangemap.o -lib/frama-c/reachingdefs.cmi -lib/frama-c/reachingdefs.cmo -lib/frama-c/reachingdefs.cmx -lib/frama-c/reachingdefs.o -lib/frama-c/rmciltmps.cmi -lib/frama-c/rmciltmps.cmo -lib/frama-c/rmciltmps.cmx -lib/frama-c/rmciltmps.o lib/frama-c/rmtmps.cmi lib/frama-c/rmtmps.cmo lib/frama-c/rmtmps.cmx @@ -679,14 +662,14 @@ lib/frama-c/slicingTypes.cmi lib/frama-c/slicingTypes.cmo lib/frama-c/slicingTypes.cmx lib/frama-c/slicingTypes.o -%%GUI%%lib/frama-c/source_manager.cmi -%%GUI%%lib/frama-c/source_manager.cmo -%%GUI%%lib/frama-c/source_manager.cmx -%%GUI%%lib/frama-c/source_manager.o -%%GUI%%lib/frama-c/source_viewer.cmi -%%GUI%%lib/frama-c/source_viewer.cmo -%%GUI%%lib/frama-c/source_viewer.cmx -%%GUI%%lib/frama-c/source_viewer.o +lib/frama-c/source_manager.cmi +lib/frama-c/source_manager.cmo +lib/frama-c/source_manager.cmx +lib/frama-c/source_manager.o +lib/frama-c/source_viewer.cmi +lib/frama-c/source_viewer.cmo +lib/frama-c/source_viewer.cmx +lib/frama-c/source_viewer.o lib/frama-c/special_hooks.cmi lib/frama-c/special_hooks.cmo lib/frama-c/special_hooks.cmx @@ -731,10 +714,10 @@ lib/frama-c/task.cmi lib/frama-c/task.cmo lib/frama-c/task.cmx lib/frama-c/task.o -%%GUI%%lib/frama-c/toolbox.cmi -%%GUI%%lib/frama-c/toolbox.cmo -%%GUI%%lib/frama-c/toolbox.cmx -%%GUI%%lib/frama-c/toolbox.o +lib/frama-c/toolbox.cmi +lib/frama-c/toolbox.cmo +lib/frama-c/toolbox.cmx +lib/frama-c/toolbox.o lib/frama-c/tr_offset.cmi lib/frama-c/tr_offset.cmo lib/frama-c/tr_offset.cmx @@ -771,10 +754,6 @@ lib/frama-c/unroll_loops.cmi lib/frama-c/unroll_loops.cmo lib/frama-c/unroll_loops.cmx lib/frama-c/unroll_loops.o -lib/frama-c/usedef.cmi -lib/frama-c/usedef.cmo -lib/frama-c/usedef.cmx -lib/frama-c/usedef.o lib/frama-c/utf8_logic.cmi lib/frama-c/utf8_logic.cmo lib/frama-c/utf8_logic.cmx @@ -795,10 +774,10 @@ lib/frama-c/visitor.cmi lib/frama-c/visitor.cmo lib/frama-c/visitor.cmx lib/frama-c/visitor.o -%%GUI%%lib/frama-c/warning_manager.cmi -%%GUI%%lib/frama-c/warning_manager.cmo -%%GUI%%lib/frama-c/warning_manager.cmx -%%GUI%%lib/frama-c/warning_manager.o +lib/frama-c/warning_manager.cmi +lib/frama-c/warning_manager.cmo +lib/frama-c/warning_manager.cmx +lib/frama-c/warning_manager.o lib/frama-c/widen_type.cmi lib/frama-c/widen_type.cmo lib/frama-c/widen_type.cmx @@ -825,19 +804,6 @@ share/emacs/site-lisp/acsl.el %%DATADIR%%/doc/code/style.css %%DATADIR%%/doc/code/toc_head.htm %%DATADIR%%/doc/code/toc_tail.htm -%%DATADIR%%/feedback/considered_valid.png -%%DATADIR%%/feedback/inconsistent.png -%%DATADIR%%/feedback/invalid_but_dead.png -%%DATADIR%%/feedback/invalid_under_hyp.png -%%DATADIR%%/feedback/never_tried.png -%%DATADIR%%/feedback/surely_invalid.png -%%DATADIR%%/feedback/surely_valid.png -%%DATADIR%%/feedback/switch-off.png -%%DATADIR%%/feedback/switch-on.png -%%DATADIR%%/feedback/unknown.png -%%DATADIR%%/feedback/unknown_but_dead.png -%%DATADIR%%/feedback/valid_but_dead.png -%%DATADIR%%/feedback/valid_under_hyp.png %%DATADIR%%/frama-c.gif %%DATADIR%%/frama-c.ico %%DATADIR%%/frama-c.rc @@ -850,6 +816,7 @@ share/emacs/site-lisp/acsl.el %%DATADIR%%/libc/__fc_define_dev_t.h %%DATADIR%%/libc/__fc_define_fd_set_t.h %%DATADIR%%/libc/__fc_define_file.h +%%DATADIR%%/libc/__fc_define_fpos_t.h %%DATADIR%%/libc/__fc_define_id_t.h %%DATADIR%%/libc/__fc_define_ino_t.h %%DATADIR%%/libc/__fc_define_intptr_t.h @@ -950,66 +917,93 @@ share/emacs/site-lisp/acsl.el %%DATADIR%%/machine.h %%DATADIR%%/math.c %%DATADIR%%/math.h +%%DATADIR%%/theme/colorblind/considered_valid.png +%%DATADIR%%/theme/colorblind/inconsistent.png +%%DATADIR%%/theme/colorblind/invalid_but_dead.png +%%DATADIR%%/theme/colorblind/invalid_under_hyp.png +%%DATADIR%%/theme/colorblind/never_tried.png +%%DATADIR%%/theme/colorblind/surely_invalid.png +%%DATADIR%%/theme/colorblind/surely_valid.png +%%DATADIR%%/theme/colorblind/switch-off.png +%%DATADIR%%/theme/colorblind/switch-on.png +%%DATADIR%%/theme/colorblind/unknown.png +%%DATADIR%%/theme/colorblind/unknown_but_dead.png +%%DATADIR%%/theme/colorblind/valid_but_dead.png +%%DATADIR%%/theme/colorblind/valid_under_hyp.png +%%DATADIR%%/theme/default/considered_valid.png +%%DATADIR%%/theme/default/inconsistent.png +%%DATADIR%%/theme/default/invalid_but_dead.png +%%DATADIR%%/theme/default/invalid_under_hyp.png +%%DATADIR%%/theme/default/never_tried.png +%%DATADIR%%/theme/default/surely_invalid.png +%%DATADIR%%/theme/default/surely_valid.png +%%DATADIR%%/theme/default/switch-off.png +%%DATADIR%%/theme/default/switch-on.png +%%DATADIR%%/theme/default/unknown.png +%%DATADIR%%/theme/default/unknown_but_dead.png +%%DATADIR%%/theme/default/valid_but_dead.png +%%DATADIR%%/theme/default/valid_under_hyp.png %%DATADIR%%/unmark.png -%%PLUGINS%%%%DATADIR%%/wp/coqwp/Bits.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/BuiltIn.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/Cbits.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/Cfloat.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/Cint.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/Cmath.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/Memory.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/Qed.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/Qedlib.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/Vset.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/Zbits.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/bool/Bool.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/int/Abs.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/int/ComputerDivision.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/int/Int.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/int/MinMax.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/map/Map.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/real/Abs.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/real/FromInt.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/real/MinMax.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/real/Real.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/real/RealInfix.v -%%PLUGINS%%%%DATADIR%%/wp/coqwp/real/Square.v -%%PLUGINS%%%%DATADIR%%/wp/ergo/Cbits.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/Cfloat.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/Cint.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/Cmath.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/Memory.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/Qed.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/Vset.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/bool.Bool.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/int.Abs.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/int.ComputerDivision.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/int.Int.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/int.MinMax.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/map.Map.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/real.Abs.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/real.FromInt.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/real.MinMax.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/real.Real.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/real.RealInfix.mlw -%%PLUGINS%%%%DATADIR%%/wp/ergo/real.Square.mlw -%%PLUGINS%%%%DATADIR%%/wp/why3/Bits.v -%%PLUGINS%%%%DATADIR%%/wp/why3/Cbits.v -%%PLUGINS%%%%DATADIR%%/wp/why3/Cbits.why -%%PLUGINS%%%%DATADIR%%/wp/why3/Cfloat.v -%%PLUGINS%%%%DATADIR%%/wp/why3/Cfloat.why -%%PLUGINS%%%%DATADIR%%/wp/why3/Cint.v -%%PLUGINS%%%%DATADIR%%/wp/why3/Cint.why -%%PLUGINS%%%%DATADIR%%/wp/why3/Cmath.v -%%PLUGINS%%%%DATADIR%%/wp/why3/Cmath.why -%%PLUGINS%%%%DATADIR%%/wp/why3/Memory.v -%%PLUGINS%%%%DATADIR%%/wp/why3/Memory.why -%%PLUGINS%%%%DATADIR%%/wp/why3/Qed.v -%%PLUGINS%%%%DATADIR%%/wp/why3/Qed.why -%%PLUGINS%%%%DATADIR%%/wp/why3/Qedlib.v -%%PLUGINS%%%%DATADIR%%/wp/why3/Vset.v -%%PLUGINS%%%%DATADIR%%/wp/why3/Vset.why -%%PLUGINS%%%%DATADIR%%/wp/why3/Zbits.v -%%PLUGINS%%%%DATADIR%%/wp/why3/coq.drv -%%PLUGINS%%%%DATADIR%%/wp/why3/why3.conf -%%PLUGINS%%%%DATADIR%%/wp/wp.driver +%%DATADIR%%/wp/coqwp/Bits.v +%%DATADIR%%/wp/coqwp/BuiltIn.v +%%DATADIR%%/wp/coqwp/Cbits.v +%%DATADIR%%/wp/coqwp/Cfloat.v +%%DATADIR%%/wp/coqwp/Cint.v +%%DATADIR%%/wp/coqwp/Cmath.v +%%DATADIR%%/wp/coqwp/Memory.v +%%DATADIR%%/wp/coqwp/Qed.v +%%DATADIR%%/wp/coqwp/Qedlib.v +%%DATADIR%%/wp/coqwp/Vset.v +%%DATADIR%%/wp/coqwp/Zbits.v +%%DATADIR%%/wp/coqwp/bool/Bool.v +%%DATADIR%%/wp/coqwp/int/Abs.v +%%DATADIR%%/wp/coqwp/int/ComputerDivision.v +%%DATADIR%%/wp/coqwp/int/Int.v +%%DATADIR%%/wp/coqwp/int/MinMax.v +%%DATADIR%%/wp/coqwp/map/Map.v +%%DATADIR%%/wp/coqwp/real/Abs.v +%%DATADIR%%/wp/coqwp/real/FromInt.v +%%DATADIR%%/wp/coqwp/real/MinMax.v +%%DATADIR%%/wp/coqwp/real/Real.v +%%DATADIR%%/wp/coqwp/real/RealInfix.v +%%DATADIR%%/wp/coqwp/real/Square.v +%%DATADIR%%/wp/ergo/Cbits.mlw +%%DATADIR%%/wp/ergo/Cfloat.mlw +%%DATADIR%%/wp/ergo/Cint.mlw +%%DATADIR%%/wp/ergo/Cmath.mlw +%%DATADIR%%/wp/ergo/Memory.mlw +%%DATADIR%%/wp/ergo/Qed.mlw +%%DATADIR%%/wp/ergo/Vset.mlw +%%DATADIR%%/wp/ergo/bool.Bool.mlw +%%DATADIR%%/wp/ergo/int.Abs.mlw +%%DATADIR%%/wp/ergo/int.ComputerDivision.mlw +%%DATADIR%%/wp/ergo/int.Int.mlw +%%DATADIR%%/wp/ergo/int.MinMax.mlw +%%DATADIR%%/wp/ergo/map.Map.mlw +%%DATADIR%%/wp/ergo/real.Abs.mlw +%%DATADIR%%/wp/ergo/real.FromInt.mlw +%%DATADIR%%/wp/ergo/real.MinMax.mlw +%%DATADIR%%/wp/ergo/real.Real.mlw +%%DATADIR%%/wp/ergo/real.RealInfix.mlw +%%DATADIR%%/wp/ergo/real.Square.mlw +%%DATADIR%%/wp/why3/Bits.v +%%DATADIR%%/wp/why3/Cbits.v +%%DATADIR%%/wp/why3/Cbits.why +%%DATADIR%%/wp/why3/Cfloat.v +%%DATADIR%%/wp/why3/Cfloat.why +%%DATADIR%%/wp/why3/Cint.v +%%DATADIR%%/wp/why3/Cint.why +%%DATADIR%%/wp/why3/Cmath.v +%%DATADIR%%/wp/why3/Cmath.why +%%DATADIR%%/wp/why3/Memory.v +%%DATADIR%%/wp/why3/Memory.why +%%DATADIR%%/wp/why3/Qed.v +%%DATADIR%%/wp/why3/Qed.why +%%DATADIR%%/wp/why3/Qedlib.v +%%DATADIR%%/wp/why3/Vset.v +%%DATADIR%%/wp/why3/Vset.why +%%DATADIR%%/wp/why3/Zbits.v +%%DATADIR%%/wp/why3/coq.drv +%%DATADIR%%/wp/why3/why3.conf +%%DATADIR%%/wp/wp.driver +@dir lib/frama-c/plugins/gui