Date: Thu, 7 Mar 2013 03:56:52 +0000 (UTC) From: Brendan Fabeny <bf@FreeBSD.org> To: ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org Subject: svn commit: r313561 - head/devel/frama-c Message-ID: <201303070356.r273uqLE092441@svn.freebsd.org>
next in thread | raw e-mail | index | archive | help
Author: bf Date: Thu Mar 7 03:56:51 2013 New Revision: 313561 URL: http://svnweb.freebsd.org/changeset/ports/313561 Log: update to the Oxygen release Modified: head/devel/frama-c/Makefile head/devel/frama-c/distinfo (contents, props changed) head/devel/frama-c/pkg-plist (contents, props changed) Modified: head/devel/frama-c/Makefile ============================================================================== --- head/devel/frama-c/Makefile Thu Mar 7 03:46:47 2013 (r313560) +++ head/devel/frama-c/Makefile Thu Mar 7 03:56:51 2013 (r313561) @@ -2,9 +2,8 @@ # $FreeBSD$ PORTNAME= frama-c -DISTVERSIONPREFIX= Nitrogen- -DISTVERSION= 20111001 -PORTREVISION= 3 +DISTVERSIONPREFIX= Oxygen- +DISTVERSION= 20120901 CATEGORIES= devel MASTER_SITES= http://frama-c.com/download/ LOCAL/bf @@ -13,21 +12,30 @@ COMMENT= Extensible platform for source- LICENSE= LGPL21 +BUILD_DEPENDS= ${LOCALBASE}/lib/ocaml/ocamlgraph/graph.a:${PORTSDIR}/math/ocaml-ocamlgraph +RUN_DEPENDS= ${LOCALBASE}/lib/ocaml/ocamlgraph/graph.a:${PORTSDIR}/math/ocaml-ocamlgraph + GNU_CONFIGURE= yes +CONFIGURE_ARGS+= --with-cpp="${FRAMAC_DEFAULT_CPP}" MAKE_ENV+= FRAMAC_LIBDIR="${PREFIX}/lib/frama-c" MAN1= frama-c.1 frama-c-gui.1 -OPTIONS= ALTERGO "Build wp plugin components that use Alt-Ergo" on \ - COQ "Build wp plugin components that use Coq" off \ - GUI "Build GUI" on \ - PLUGINS "Build bundled plugins" on + +OPTIONS_DEFINE= ALTERGO COQ GUI PLUGINS +OPTIONS_DEFAULT= ALTERGO GUI PLUGINS +ALTERGO_DESC= Alt-Ergo plugin (requires PLUGINS) +COQ_DESC= Coq plugin (requires PLUGINS) +GUI_DESC= Graphical User Interface (requires PLUGINS) + USE_GMAKE= yes USE_OCAML= yes .include <bsd.port.options.mk> -.if defined(WITH_ALTERGO) -.if !defined(WITH_PLUGINS) -IGNORE = requires WITH_PLUGINS for WITH_ALTERGO +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 @@ -35,9 +43,9 @@ RUN_DEPENDS+= alt-ergo:${PORTSDIR}/math CONFIGURE_ENV += HAS_ALTERGO=no .endif -.if defined(WITH_COQ) -.if !defined(WITH_PLUGINS) -IGNORE = requires WITH_PLUGINS for WITH_COQ +.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 @@ -45,9 +53,9 @@ RUN_DEPENDS+= coqc:${PORTSDIR}/math/coq CONFIGURE_ENV += HAS_COQ=no .endif -.if defined(WITH_GUI) -.if !defined(WITH_PLUGINS) -IGNORE = requires WITH_PLUGINS for WITH_GUI +.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 @@ -58,7 +66,7 @@ CONFIGURE_ARGS+= --disable-gui PLIST_SUB+= GUI="@comment " .endif -.if defined(WITH_PLUGINS) +.if ${PORT_OPTIONS:MPLUGINS} BUILD_DEPENDS += dot:${PORTSDIR}/graphics/graphviz \ ltl2ba:${PORTSDIR}/math/ltl2ba RUN_DEPENDS+= dot:${PORTSDIR}/graphics/graphviz \ @@ -69,20 +77,9 @@ CONFIGURE_ARGS+= --with-no-plugin PLIST_SUB+= PLUGINS="@comment " .endif -post-extract: - @cd ${WRKSRC}; ${EXTRACT_CMD} ${EXTRACT_BEFORE_ARGS} \ - ocamlgraph.tar.gz ${EXTRACT_AFTER_ARGS} - post-patch: - @${MKDIR} ${WRKSRC}/tests/report \ - ${WRKSRC}/tests/wp \ - ${WRKSRC}/tests/wp_plugin \ - ${WRKSRC}/tests/wp_acsl \ - ${WRKSRC}/tests/wp_store \ - ${WRKSRC}/tests/wp_hoare \ - ${WRKSRC}/tests/wp_runtime \ - ${WRKSRC}/tests/wp_bts \ - ${WRKSRC}/tests/wp_engine + @cd ${WRKSRC}/tests; ${MKDIR} aorai report wp wp_acsl wp_bts \ + wp_engine wp_hoare wp_plugin wp_runtime wp_store wp_typed @${REINPLACE_CMD} -e 's|@make |@${GMAKE} |' \ ${WRKSRC}/src/aorai/Makefile.in @${REINPLACE_CMD} \ @@ -95,11 +92,7 @@ post-patch: ${WRKSRC}/share/Makefile.dynamic @${REINPLACE_CMD} -e '\|^# Installation|,\|^# File headers|{ \ \|$$(CP).*bin|s|$$(CP)|${INSTALL_SCRIPT}|; \ - \|$$(CP) -R doc/manuals $$(FRAMAC_DATADIR)| \ - s||${MKDIR} $$(FRAMAC_DATADIR)/manuals ; \ - ${INSTALL_DATA} doc/manuals/* $$(FRAMAC_DATADIR)/manuals|; \ - \|$$(CP).*man|s|$$(CP)\( -R\)*|${INSTALL_MAN}|; \ - \|$$(CP).*share|s|$$(CP)\( -R\)*|${INSTALL_DATA}|; \ + \|$$(CP).*man/|s|$$(CP)|${INSTALL_MAN}|; \ s|$$(CP)|${INSTALL_DATA}|; }' \ ${WRKSRC}/Makefile @${REINPLACE_CMD} -e 's|HAS_ALTERGO=$$||' \ @@ -107,14 +100,9 @@ post-patch: -e 's|HAS_COQ=$$||' \ ${WRKSRC}/configure @${REINPLACE_CMD} -Ee 's@(\+|/)(lablgtk2)@\1site-lib/\2@' \ - ${WRKSRC}/Makefile \ - ${WRKSRC}/configure \ - ${WRKSRC}/ocamlgraph/configure \ - ${WRKSRC}/ocamlgraph/view_graph/Makefile \ - ${WRKSRC}/share/Makefile.plugin \ ${WRKSRC}/src/kernel/dynamic.ml -.if defined(WITH_GUI) +.if ${PORT_OPTIONS:MGUI} pre-configure: @(if [ ! -e ${LOCALBASE}/${OCAML_SITELIBDIR}/lablgtk2/gtkSourceView2.cmi -o \ ! -e ${LOCALBASE}/${OCAML_SITELIBDIR}/lablgtk2/gnomeCanvas.cmi ] ; then \ @@ -133,14 +121,9 @@ post-install: @${TOUCH} ${PREFIX}/lib/frama-c/plugins/.keep_me \ ${PREFIX}/lib/frama-c/plugins/gui/.keep_me -.if defined(MAINTAINER_MODE) check regression-test test: build - @(cd ${WRKSRC}; ${SETENV} ${MAKE_ENV} \ - FRAMAC_LIB=${WRKSRC}/lib/fc \ - FRAMAC_PLUGIN=${WRKSRC}/lib/plugins \ - FRAMAC_SHARE=${WRKSRC}/share \ - ${GMAKE} ${_MAKE_JOBS} ${MAKE_ARGS} tests) - -.endif + @cd ${WRKSRC}; ${SETENV} ${MAKE_ENV:NCPP=*} \ + CPP="${CPP} -C -I${WRKSRC}/share/libc -I." \ + ${GMAKE} ${MAKE_ARGS} oracles fulltests .include <bsd.port.mk> Modified: head/devel/frama-c/distinfo ============================================================================== --- head/devel/frama-c/distinfo Thu Mar 7 03:46:47 2013 (r313560) +++ head/devel/frama-c/distinfo Thu Mar 7 03:56:51 2013 (r313561) @@ -1,2 +1,2 @@ -SHA256 (frama-c-Nitrogen-20111001.tar.gz) = 8afad848321c958fab265045cd152482e77ce7c175ee7c9af2d4bec57a1bc671 -SIZE (frama-c-Nitrogen-20111001.tar.gz) = 12110786 +SHA256 (frama-c-Oxygen-20120901.tar.gz) = f749870a2451f97d24da886c0cc7708e3ec57ad3f169f6b79f9b52be1f47c216 +SIZE (frama-c-Oxygen-20120901.tar.gz) = 10815011 Modified: head/devel/frama-c/pkg-plist ============================================================================== --- head/devel/frama-c/pkg-plist Thu Mar 7 03:46:47 2013 (r313560) +++ head/devel/frama-c/pkg-plist Thu Mar 7 03:56:51 2013 (r313561) @@ -19,7 +19,6 @@ bin/ptests.byte %%GUI%%lib/frama-c/design.cmo %%GUI%%lib/frama-c/design.cmx %%GUI%%lib/frama-c/design.o -%%GUI%%lib/frama-c/dgraph.cmi %%GUI%%lib/frama-c/file_manager.cmi %%GUI%%lib/frama-c/file_manager.cmo %%GUI%%lib/frama-c/file_manager.cmx @@ -60,8 +59,8 @@ bin/ptests.byte %%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.cmo %%GUI%%lib/frama-c/plugins/gui/Wp.cmxs %%GUI%%lib/frama-c/pretty_source.cmi %%GUI%%lib/frama-c/pretty_source.cmo @@ -138,27 +137,30 @@ bin/ptests.byte %%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 %%PLUGINS%%lib/frama-c/plugins/Security_slicing.cmi %%PLUGINS%%lib/frama-c/plugins/Security_slicing.cmo %%PLUGINS%%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.cmo %%PLUGINS%%lib/frama-c/plugins/Wp.cmxs lib/frama-c/abstract_interp.cmi lib/frama-c/abstract_interp.cmo lib/frama-c/abstract_interp.cmx lib/frama-c/abstract_interp.o -lib/frama-c/abstract_value.cmi -lib/frama-c/abstract_value.cmo -lib/frama-c/abstract_value.cmx -lib/frama-c/abstract_value.o lib/frama-c/alarms.cmi lib/frama-c/alarms.cmo lib/frama-c/alarms.cmx lib/frama-c/alarms.o +lib/frama-c/allocates.cmi +lib/frama-c/allocates.cmo +lib/frama-c/allocates.cmx +lib/frama-c/allocates.o lib/frama-c/alpha.cmi lib/frama-c/alpha.cmo lib/frama-c/alpha.cmx @@ -228,6 +230,10 @@ lib/frama-c/cabs2cil.cmi lib/frama-c/cabs2cil.cmo lib/frama-c/cabs2cil.cmx lib/frama-c/cabs2cil.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 @@ -277,10 +283,6 @@ lib/frama-c/cilmsg.cmi lib/frama-c/cilmsg.cmo lib/frama-c/cilmsg.cmx lib/frama-c/cilmsg.o -lib/frama-c/ciltools.cmi -lib/frama-c/ciltools.cmo -lib/frama-c/ciltools.cmx -lib/frama-c/ciltools.o lib/frama-c/cilutil.cmi lib/frama-c/cilutil.cmo lib/frama-c/cilutil.cmx @@ -317,10 +319,6 @@ lib/frama-c/cvalue.cmi lib/frama-c/cvalue.cmo lib/frama-c/cvalue.cmx lib/frama-c/cvalue.o -lib/frama-c/dashtbl.cmi -lib/frama-c/dashtbl.cmo -lib/frama-c/dashtbl.cmx -lib/frama-c/dashtbl.o lib/frama-c/dataflow.cmi lib/frama-c/dataflow.cmo lib/frama-c/dataflow.cmx @@ -385,6 +383,10 @@ lib/frama-c/filter.cmi lib/frama-c/filter.cmo lib/frama-c/filter.cmx lib/frama-c/filter.o +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/frontc.cmi lib/frama-c/frontc.cmo lib/frama-c/frontc.cmx @@ -397,14 +399,14 @@ lib/frama-c/globals.cmi lib/frama-c/globals.cmo lib/frama-c/globals.cmx lib/frama-c/globals.o -lib/frama-c/graph.cmi -lib/frama-c/graph.cmo -lib/frama-c/graph.cmx -lib/frama-c/graph.o lib/frama-c/growArray.cmi lib/frama-c/growArray.cmo lib/frama-c/growArray.cmx lib/frama-c/growArray.o +lib/frama-c/hashtbl_common_interface.cmi +lib/frama-c/hashtbl_common_interface.cmo +lib/frama-c/hashtbl_common_interface.cmx +lib/frama-c/hashtbl_common_interface.o lib/frama-c/hook.cmi lib/frama-c/hook.cmo lib/frama-c/hook.cmx @@ -417,6 +419,10 @@ lib/frama-c/hptset.cmi lib/frama-c/hptset.cmo lib/frama-c/hptset.cmx lib/frama-c/hptset.o +lib/frama-c/indexer.cmi +lib/frama-c/indexer.cmo +lib/frama-c/indexer.cmx +lib/frama-c/indexer.o lib/frama-c/infer_annotations.cmi lib/frama-c/infer_annotations.cmo lib/frama-c/infer_annotations.cmx @@ -437,10 +443,6 @@ 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/inthash.cmi -lib/frama-c/inthash.cmo -lib/frama-c/inthash.cmx -lib/frama-c/inthash.o lib/frama-c/ival.cmi lib/frama-c/ival.cmo lib/frama-c/ival.cmx @@ -600,10 +602,6 @@ lib/frama-c/parameter.cmi lib/frama-c/parameter.cmo lib/frama-c/parameter.cmx lib/frama-c/parameter.o -lib/frama-c/path_lattice.cmi -lib/frama-c/path_lattice.cmo -lib/frama-c/path_lattice.cmx -lib/frama-c/path_lattice.o lib/frama-c/pdgIndex.cmi lib/frama-c/pdgIndex.cmo lib/frama-c/pdgIndex.cmx @@ -679,10 +677,6 @@ lib/frama-c/setWithNearest.cmi lib/frama-c/setWithNearest.cmo lib/frama-c/setWithNearest.cmx lib/frama-c/setWithNearest.o -lib/frama-c/shifted_Location.cmi -lib/frama-c/shifted_Location.cmo -lib/frama-c/shifted_Location.cmx -lib/frama-c/shifted_Location.o lib/frama-c/slicingInternals.cmi lib/frama-c/slicingInternals.cmo lib/frama-c/slicingInternals.cmx @@ -707,22 +701,18 @@ lib/frama-c/state_dependency_graph.cmi lib/frama-c/state_dependency_graph.cmo lib/frama-c/state_dependency_graph.cmx lib/frama-c/state_dependency_graph.o -lib/frama-c/state_imp.cmi -lib/frama-c/state_imp.cmo -lib/frama-c/state_imp.cmx -lib/frama-c/state_imp.o lib/frama-c/state_selection.cmi lib/frama-c/state_selection.cmo lib/frama-c/state_selection.cmx lib/frama-c/state_selection.o -lib/frama-c/state_set.cmi -lib/frama-c/state_set.cmo -lib/frama-c/state_set.cmx -lib/frama-c/state_set.o lib/frama-c/state_topological.cmi lib/frama-c/state_topological.cmo lib/frama-c/state_topological.cmx lib/frama-c/state_topological.o +lib/frama-c/statuses_by_call.cmi +lib/frama-c/statuses_by_call.cmo +lib/frama-c/statuses_by_call.cmx +lib/frama-c/statuses_by_call.o lib/frama-c/stmts_graph.cmi lib/frama-c/stmts_graph.cmo lib/frama-c/stmts_graph.cmx @@ -775,6 +765,10 @@ lib/frama-c/utf8_logic.cmi lib/frama-c/utf8_logic.cmo lib/frama-c/utf8_logic.cmx lib/frama-c/utf8_logic.o +lib/frama-c/value_aux.cmi +lib/frama-c/value_aux.cmo +lib/frama-c/value_aux.cmx +lib/frama-c/value_aux.o lib/frama-c/visitor.cmi lib/frama-c/visitor.cmo lib/frama-c/visitor.cmx @@ -783,10 +777,6 @@ lib/frama-c/whitetrack.cmi lib/frama-c/whitetrack.cmo lib/frama-c/whitetrack.cmx lib/frama-c/whitetrack.o -lib/frama-c/widen.cmi -lib/frama-c/widen.cmo -lib/frama-c/widen.cmx -lib/frama-c/widen.o lib/frama-c/widen_type.cmi lib/frama-c/widen_type.cmo lib/frama-c/widen_type.cmx @@ -801,14 +791,15 @@ share/emacs/site-lisp/acsl.el %%DATADIR%%/acsl.el %%DATADIR%%/builtin.c %%DATADIR%%/builtin.h -%%DATADIR%%/check.png %%DATADIR%%/configure.ac +%%DATADIR%%/doc/code/docgen_ge400.ml +%%DATADIR%%/doc/code/docgen_lt400.ml %%DATADIR%%/doc/code/intro_kernel_plugin.txt %%DATADIR%%/doc/code/intro_plugin.txt +%%DATADIR%%/doc/code/intro_plugin_default.txt %%DATADIR%%/doc/code/style.css %%DATADIR%%/doc/code/toc_head.htm %%DATADIR%%/doc/code/toc_tail.htm -%%DATADIR%%/failed.png %%DATADIR%%/feedback/considered_valid.png %%DATADIR%%/feedback/inconsistent.png %%DATADIR%%/feedback/invalid_but_dead.png @@ -824,14 +815,16 @@ share/emacs/site-lisp/acsl.el %%DATADIR%%/frama-c.gif %%DATADIR%%/frama-c.ico %%DATADIR%%/frama-c.rc -%%DATADIR%%/left.png %%DATADIR%%/libc.c %%DATADIR%%/libc.h %%DATADIR%%/libc/__fc_builtin.c %%DATADIR%%/libc/__fc_builtin.h +%%DATADIR%%/libc/__fc_builtin_for_normalization.i %%DATADIR%%/libc/__fc_define_blkcnt_t.h %%DATADIR%%/libc/__fc_define_blksize_t.h %%DATADIR%%/libc/__fc_define_dev_t.h +%%DATADIR%%/libc/__fc_define_fd_set_t.h +%%DATADIR%%/libc/__fc_define_id_t.h %%DATADIR%%/libc/__fc_define_ino_t.h %%DATADIR%%/libc/__fc_define_intptr_t.h %%DATADIR%%/libc/__fc_define_iovec.h @@ -841,42 +834,63 @@ share/emacs/site-lisp/acsl.el %%DATADIR%%/libc/__fc_define_off_t.h %%DATADIR%%/libc/__fc_define_pid_t.h %%DATADIR%%/libc/__fc_define_restrict.h +%%DATADIR%%/libc/__fc_define_sa_family_t.h +%%DATADIR%%/libc/__fc_define_seek_macros.h +%%DATADIR%%/libc/__fc_define_sigset_t.h %%DATADIR%%/libc/__fc_define_size_t.h +%%DATADIR%%/libc/__fc_define_sockaddr.h %%DATADIR%%/libc/__fc_define_ssize_t.h %%DATADIR%%/libc/__fc_define_suseconds_t.h %%DATADIR%%/libc/__fc_define_time_t.h +%%DATADIR%%/libc/__fc_define_timespec.h %%DATADIR%%/libc/__fc_define_uid_and_gid.h %%DATADIR%%/libc/__fc_define_useconds_t.h %%DATADIR%%/libc/__fc_define_wchar_t.h %%DATADIR%%/libc/__fc_machdep.h %%DATADIR%%/libc/__fc_string_axiomatic.h +%%DATADIR%%/libc/arpa/inet.c +%%DATADIR%%/libc/arpa/inet.h %%DATADIR%%/libc/assert.c %%DATADIR%%/libc/assert.h %%DATADIR%%/libc/complex.c %%DATADIR%%/libc/complex.h %%DATADIR%%/libc/ctype.c %%DATADIR%%/libc/ctype.h +%%DATADIR%%/libc/dirent.c %%DATADIR%%/libc/dirent.h %%DATADIR%%/libc/errno.c %%DATADIR%%/libc/errno.h %%DATADIR%%/libc/fc_posix_runtime.c %%DATADIR%%/libc/fc_runtime.c +%%DATADIR%%/libc/fcntl.c %%DATADIR%%/libc/fcntl.h %%DATADIR%%/libc/fenv.c %%DATADIR%%/libc/fenv.h %%DATADIR%%/libc/float.c %%DATADIR%%/libc/float.h +%%DATADIR%%/libc/iconv.c +%%DATADIR%%/libc/iconv.h +%%DATADIR%%/libc/ifaddrs.c +%%DATADIR%%/libc/ifaddrs.h %%DATADIR%%/libc/inttypes.c %%DATADIR%%/libc/inttypes.h %%DATADIR%%/libc/iso646.c %%DATADIR%%/libc/iso646.h %%DATADIR%%/libc/limits.c %%DATADIR%%/libc/limits.h +%%DATADIR%%/libc/linux/fs.c +%%DATADIR%%/libc/linux/fs.h %%DATADIR%%/libc/locale.c %%DATADIR%%/libc/locale.h %%DATADIR%%/libc/math.c %%DATADIR%%/libc/math.h +%%DATADIR%%/libc/net/if.c +%%DATADIR%%/libc/net/if.h +%%DATADIR%%/libc/netinet/in.c %%DATADIR%%/libc/netinet/in.h +%%DATADIR%%/libc/nl_types.c +%%DATADIR%%/libc/nl_types.h +%%DATADIR%%/libc/pwd.c %%DATADIR%%/libc/pwd.h %%DATADIR%%/libc/setjmp.c %%DATADIR%%/libc/setjmp.h @@ -888,6 +902,7 @@ share/emacs/site-lisp/acsl.el %%DATADIR%%/libc/stdbool.h %%DATADIR%%/libc/stddef.c %%DATADIR%%/libc/stddef.h +%%DATADIR%%/libc/stdint.c %%DATADIR%%/libc/stdint.h %%DATADIR%%/libc/stdio.c %%DATADIR%%/libc/stdio.h @@ -895,13 +910,33 @@ share/emacs/site-lisp/acsl.el %%DATADIR%%/libc/stdlib.h %%DATADIR%%/libc/string.c %%DATADIR%%/libc/string.h +%%DATADIR%%/libc/strings.c +%%DATADIR%%/libc/strings.h +%%DATADIR%%/libc/sys/ioctl.c +%%DATADIR%%/libc/sys/ioctl.h +%%DATADIR%%/libc/sys/param.c +%%DATADIR%%/libc/sys/param.h +%%DATADIR%%/libc/sys/resource.c +%%DATADIR%%/libc/sys/resource.h +%%DATADIR%%/libc/sys/select.c +%%DATADIR%%/libc/sys/select.h +%%DATADIR%%/libc/sys/socket.c %%DATADIR%%/libc/sys/socket.h +%%DATADIR%%/libc/sys/stat.c %%DATADIR%%/libc/sys/stat.h +%%DATADIR%%/libc/sys/time.c %%DATADIR%%/libc/sys/time.h +%%DATADIR%%/libc/sys/types.c %%DATADIR%%/libc/sys/types.h +%%DATADIR%%/libc/sys/uio.c %%DATADIR%%/libc/sys/uio.h +%%DATADIR%%/libc/sys/un.c +%%DATADIR%%/libc/sys/un.h +%%DATADIR%%/libc/sys/wait.c %%DATADIR%%/libc/sys/wait.h +%%DATADIR%%/libc/syslog.c %%DATADIR%%/libc/syslog.h +%%DATADIR%%/libc/termios.c %%DATADIR%%/libc/termios.h %%DATADIR%%/libc/test.c %%DATADIR%%/libc/tgmath.c @@ -910,6 +945,7 @@ share/emacs/site-lisp/acsl.el %%DATADIR%%/libc/time.h %%DATADIR%%/libc/uchar.c %%DATADIR%%/libc/uchar.h +%%DATADIR%%/libc/unistd.c %%DATADIR%%/libc/unistd.h %%DATADIR%%/libc/wchar.c %%DATADIR%%/libc/wchar.h @@ -920,27 +956,37 @@ share/emacs/site-lisp/acsl.el %%DATADIR%%/manuals/acsl-implementation.pdf %%DATADIR%%/manuals/acsl.pdf %%DATADIR%%/manuals/aorai-manual.pdf -%%DATADIR%%/manuals/jessie-tutorial.pdf %%DATADIR%%/manuals/metrics-manual.pdf %%DATADIR%%/manuals/plugin-development-guide.pdf %%DATADIR%%/manuals/rte-manual.pdf %%DATADIR%%/manuals/user-manual.pdf %%DATADIR%%/manuals/value-analysis.pdf %%DATADIR%%/manuals/wp-manual.pdf +%%DATADIR%%/manuals/wp-tutorial.pdf %%DATADIR%%/math.c %%DATADIR%%/math.h -%%DATADIR%%/maybe.png -%%DATADIR%%/right.png %%DATADIR%%/unmark.png +%%PLUGINS%%%%DATADIR%%/wp/Cfloat.v +%%PLUGINS%%%%DATADIR%%/wp/Cint.v +%%PLUGINS%%%%DATADIR%%/wp/Cmath.v +%%PLUGINS%%%%DATADIR%%/wp/Memory.v +%%PLUGINS%%%%DATADIR%%/wp/Qedlib.v +%%PLUGINS%%%%DATADIR%%/wp/Vset.v +%%PLUGINS%%%%DATADIR%%/wp/cfloat.mlw +%%PLUGINS%%%%DATADIR%%/wp/cint.mlw +%%PLUGINS%%%%DATADIR%%/wp/cmath.mlw %%PLUGINS%%%%DATADIR%%/wp/hoare_ergo.why %%PLUGINS%%%%DATADIR%%/wp/hoare_model.v %%PLUGINS%%%%DATADIR%%/wp/hoare_model.why +%%PLUGINS%%%%DATADIR%%/wp/memory.mlw +%%PLUGINS%%%%DATADIR%%/wp/qed.mlw %%PLUGINS%%%%DATADIR%%/wp/runtime_ergo.why %%PLUGINS%%%%DATADIR%%/wp/runtime_model.v %%PLUGINS%%%%DATADIR%%/wp/runtime_model.why %%PLUGINS%%%%DATADIR%%/wp/store_ergo.why %%PLUGINS%%%%DATADIR%%/wp/store_model.v %%PLUGINS%%%%DATADIR%%/wp/store_model.why +%%PLUGINS%%%%DATADIR%%/wp/vset.mlw %%PLUGINS%%%%DATADIR%%/wp/wp.v @dirrm lib/frama-c/plugins/gui @dirrm lib/frama-c/plugins @@ -949,6 +995,9 @@ share/emacs/site-lisp/acsl.el @dirrm %%DATADIR%%/manuals @dirrm %%DATADIR%%/libc/sys @dirrm %%DATADIR%%/libc/netinet +@dirrm %%DATADIR%%/libc/net +@dirrm %%DATADIR%%/libc/linux +@dirrm %%DATADIR%%/libc/arpa @dirrm %%DATADIR%%/libc @dirrm %%DATADIR%%/feedback @dirrm %%DATADIR%%/doc/code
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?201303070356.r273uqLE092441>