pkgsrc-Changes-HG archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
[pkgsrc/trunk]: pkgsrc/devel/frama-c Updated devel/frama-c to its latest vers...
details: https://anonhg.NetBSD.org/pkgsrc/rev/76af82c75ee0
branches: trunk
changeset: 609701:76af82c75ee0
user: jaapb <jaapb%pkgsrc.org@localhost>
date: Mon Oct 08 15:28:03 2012 +0000
description:
Updated devel/frama-c to its latest version. Changes include:
-! Kernel [2012/09/17] Remove useless negative options -no-help,
-no-version, -no-print-share-path, -no-print-lib-path and
-no-print-plugin-path.
o!* Cil [2012/09/12] Split constants of logic and C (fixes bts #745).
o! Cil [2012/09/12] Remove type Cil_type.typsig. Use the functions in
Cil_datatype.Typ and Cil_datatype.Logic_typ to compare types.
o! Kernel [2012/09/03] Remove obsolete constructors Cabs.TRANSFORMER and
Cabs.EXPRTRANSFORMER and related parsing rules.
o! Value [2012/08/29] Signature change for function
Db.Value.register_builtin: builtins can now return multiple
states.
o! Value [2012/08/20] Rename Db.Value.assigns_to_zone_inputs_state to
Db.Value.assigns_inputs_to_zone. Add new functions
Db.Value.assigns_outputs_to_zone and
Db.Value.assigns_inputs_to_locations.
o!* Kernel [2012/07/31] Operations that silently mutate AST should now call
Ast.mark_as_changed to clear states depending on it
(fixes #!1244).
-! Inout [2012/07/22] Option -inout-callwise restarts Value when it is
newly set
o! Cil [2012/07/16] Ast changed: Unrool_level renamed into Unroll_specs
and its argument becomes a list for next evolutions.
o! Kernel [2012/07/16] Add function [stmt_can_reach] to the arguments
of Dataflow.Backwards, which is used to speed up the analysis.
See dataflow.mli for good possible values.
-! Rte [2012/07/16] Rename option -rte-const into
-rte-no-trivial-annotations (set by default).
-! Value [2012/07/12] More thorough checks for calls through a function
pointer: warn when the function type and the pointer are
not compatible, and stop when they cannot be reconciled.
-! Kernel [2012/07/12] A negative value given to -ulevel option hides all
UNROLL_LOOP pragmas.
+! Kernel [2012/07/10] Change semantics of 'reachable' properties
for functions. Use intrinsic notion instead of accessibility
of first statement.
o! Kernel [2012/06/25] Correct (albeit slow) hash function for terms
and term lvalues.
-! Kernel [2012/06/22] improve 'reachable' properties.
o! Kernel [2012/06/19] Remove module Inthash. Use Datatype.Int.Hashtbl
instead, or directly carbon2nitrogen.sh migration script.
o! Value [2012/06/18] Made type Ival.tt private.
o! Kernel [2012/06/11] New API for Annotations which merges old
Annotations, Globals.Annotations and operations of Kernel_function
over function contracts.
-! Pdg [2012/06/08] Rename option -dot-pdg into -pdg-dot
o! Kernel [2012/05/30] Kernel.Functions.get does not silently create
a kernel function if it does not already exist. This behavior
is kept for Cil builtins.
o! Kernel [2012/04/26] Plugin.set_optional_help is now deprecated.
*! Kernel [2012/04/14] Introduce more temporaries for a call [lv = f()] if
the return type of f and the type of lv do not match. Fix
issue #1024.
o! Kernel [2012/03/26] Kernel.CppExtraArgs now gets type
Plugin.String_list and not Plugin.String_set (fixed bts #!1132).
-! Kernel [2012/02/29] Adding some more supports for built-in related to
memory blocks.
-! Cil [2012/02/24] Functions returning a value cannot let control flow
falling through the closing '}' Fixes #685.
-! Kernel [2012/02/23] Sets generated assigns clauses into the default
behavior.
-! Kernel [2012/02/08] Adding supports for clause allocates and frees
and their version for loops.
o! Value [2011/12/02] Moved contents of memory_state/Abstract_value
into ai/Lattice_Interval_Set. Use bin/nitrogen2oxygen for
automatic migration.
-*! Kernel [2011/11/07] empty list in complete/disjoint is expanded by
logic type-checker to the list of behavior name of current
contract. Fixes issue #1006. See bts comments for the
differences that can appear in the treatment of specs.
o! Cil [2011/11/04] Add method pFile in printers. Signature change for
Cil.d_file (but you should use !Ast_printer.d_file).
o! Kernel [2011/10/18] Logic_preprocess.file takes an additional parameter,
as gcc pre-processor treats differently .c and .cxx files,
and this must be reflected in annotation pre-processing.
diffstat:
devel/frama-c/Makefile | 7 +-
devel/frama-c/PLIST | 185 +++++++++++++++++++++++++++++++++++++-----------
devel/frama-c/distinfo | 10 +-
3 files changed, 149 insertions(+), 53 deletions(-)
diffs (truncated from 467 to 300 lines):
diff -r 4b6f06e5e2da -r 76af82c75ee0 devel/frama-c/Makefile
--- a/devel/frama-c/Makefile Mon Oct 08 15:21:33 2012 +0000
+++ b/devel/frama-c/Makefile Mon Oct 08 15:28:03 2012 +0000
@@ -1,9 +1,8 @@
-# $NetBSD: Makefile,v 1.27 2012/10/02 17:10:46 tron Exp $
+# $NetBSD: Makefile,v 1.28 2012/10/08 15:28:03 jaapb Exp $
#
-DISTNAME= frama-c-Nitrogen-20111001
-PKGNAME= ${DISTNAME:S/-Nitrogen//}
-PKGREVISION= 11
+DISTNAME= frama-c-Oxygen-20120901
+PKGNAME= ${DISTNAME:S/-Oxygen//}
CATEGORIES= devel
MASTER_SITES= http://frama-c.com/download/
diff -r 4b6f06e5e2da -r 76af82c75ee0 devel/frama-c/PLIST
--- a/devel/frama-c/PLIST Mon Oct 08 15:21:33 2012 +0000
+++ b/devel/frama-c/PLIST Mon Oct 08 15:28:03 2012 +0000
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.3 2011/12/25 15:52:12 asau Exp $
+@comment $NetBSD: PLIST,v 1.4 2012/10/08 15:28:04 jaapb Exp $
bin/frama-c
${PLIST.gui}bin/frama-c-gui
${PLIST.gui}bin/frama-c-gui.byte
@@ -56,14 +56,18 @@
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
+@comment lib/frama-c/abstract_value.cmi
+@comment lib/frama-c/abstract_value.cmo
+@comment lib/frama-c/abstract_value.cmx
+@comment 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
@@ -141,6 +145,10 @@
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
@@ -190,10 +198,10 @@
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
+@comment lib/frama-c/ciltools.cmi
+@comment lib/frama-c/ciltools.cmo
+@comment lib/frama-c/ciltools.cmx
+@comment lib/frama-c/ciltools.o
lib/frama-c/cilutil.cmi
lib/frama-c/cilutil.cmo
lib/frama-c/cilutil.cmx
@@ -230,10 +238,10 @@
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
+@comment lib/frama-c/dashtbl.cmi
+@comment lib/frama-c/dashtbl.cmo
+@comment lib/frama-c/dashtbl.cmx
+@comment lib/frama-c/dashtbl.o
lib/frama-c/dataflow.cmi
lib/frama-c/dataflow.cmo
lib/frama-c/dataflow.cmx
@@ -315,6 +323,10 @@
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
@@ -356,6 +368,10 @@
${PLIST.gui}lib/frama-c/history.cmo
${PLIST.gui}lib/frama-c/history.cmx
${PLIST.gui}lib/frama-c/history.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
@@ -368,6 +384,10 @@
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
@@ -388,10 +408,10 @@
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
+@comment lib/frama-c/inthash.cmi
+@comment lib/frama-c/inthash.cmo
+@comment lib/frama-c/inthash.cmx
+@comment lib/frama-c/inthash.o
lib/frama-c/ival.cmi
lib/frama-c/ival.cmo
lib/frama-c/ival.cmx
@@ -559,10 +579,10 @@
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
+@comment lib/frama-c/path_lattice.cmi
+@comment lib/frama-c/path_lattice.cmo
+@comment lib/frama-c/path_lattice.cmx
+@comment lib/frama-c/path_lattice.o
lib/frama-c/pdgIndex.cmi
lib/frama-c/pdgIndex.cmo
lib/frama-c/pdgIndex.cmx
@@ -582,20 +602,25 @@
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.cmo
+@comment lib/frama-c/plugins/Wp.cmo
lib/frama-c/plugins/Wp.cmxs
${PLIST.gui}lib/frama-c/plugins/gui/Security_slicing.cmi
${PLIST.gui}lib/frama-c/plugins/gui/Security_slicing.cmo
${PLIST.gui}lib/frama-c/plugins/gui/Security_slicing.cmxs
+${PLIST.gui}lib/frama-c/plugins/gui/Wp.cma
${PLIST.gui}lib/frama-c/plugins/gui/Wp.cmi
-${PLIST.gui}lib/frama-c/plugins/gui/Wp.cmo
+@comment ${PLIST.gui}lib/frama-c/plugins/gui/Wp.cmo
${PLIST.gui}lib/frama-c/plugins/gui/Wp.cmxs
${PLIST.gui}lib/frama-c/pretty_source.cmi
${PLIST.gui}lib/frama-c/pretty_source.cmo
@@ -666,10 +691,10 @@
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
+@comment lib/frama-c/shifted_Location.cmi
+@comment lib/frama-c/shifted_Location.cmo
+@comment lib/frama-c/shifted_Location.cmx
+@comment lib/frama-c/shifted_Location.o
lib/frama-c/slicingInternals.cmi
lib/frama-c/slicingInternals.cmo
lib/frama-c/slicingInternals.cmx
@@ -702,22 +727,26 @@
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
+@comment lib/frama-c/state_imp.cmi
+@comment lib/frama-c/state_imp.cmo
+@comment lib/frama-c/state_imp.cmx
+@comment 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
+@comment lib/frama-c/state_set.cmi
+@comment lib/frama-c/state_set.cmo
+@comment lib/frama-c/state_set.cmx
+@comment 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
@@ -770,6 +799,10 @@
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
@@ -782,10 +815,10 @@
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
+@comment lib/frama-c/widen.cmi
+@comment lib/frama-c/widen.cmo
+@comment lib/frama-c/widen.cmx
+@comment 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 +834,17 @@
share/frama-c/acsl.el
share/frama-c/builtin.c
share/frama-c/builtin.h
-share/frama-c/check.png
+@comment share/frama-c/check.png
share/frama-c/configure.ac
+share/frama-c/doc/code/docgen_ge400.ml
+share/frama-c/doc/code/docgen_lt400.ml
share/frama-c/doc/code/intro_kernel_plugin.txt
share/frama-c/doc/code/intro_plugin.txt
+share/frama-c/doc/code/intro_plugin_default.txt
share/frama-c/doc/code/style.css
share/frama-c/doc/code/toc_head.htm
share/frama-c/doc/code/toc_tail.htm
-share/frama-c/failed.png
+@comment share/frama-c/failed.png
share/frama-c/feedback/considered_valid.png
share/frama-c/feedback/inconsistent.png
share/frama-c/feedback/invalid_but_dead.png
@@ -824,14 +860,17 @@
share/frama-c/frama-c.gif
share/frama-c/frama-c.ico
share/frama-c/frama-c.rc
-share/frama-c/left.png
+@comment share/frama-c/left.png
share/frama-c/libc.c
share/frama-c/libc.h
share/frama-c/libc/__fc_builtin.c
share/frama-c/libc/__fc_builtin.h
+share/frama-c/libc/__fc_builtin_for_normalization.i
share/frama-c/libc/__fc_define_blkcnt_t.h
share/frama-c/libc/__fc_define_blksize_t.h
share/frama-c/libc/__fc_define_dev_t.h
+share/frama-c/libc/__fc_define_fd_set_t.h
+share/frama-c/libc/__fc_define_id_t.h
share/frama-c/libc/__fc_define_ino_t.h
share/frama-c/libc/__fc_define_intptr_t.h
share/frama-c/libc/__fc_define_iovec.h
@@ -841,26 +880,35 @@
share/frama-c/libc/__fc_define_off_t.h
share/frama-c/libc/__fc_define_pid_t.h
share/frama-c/libc/__fc_define_restrict.h
+share/frama-c/libc/__fc_define_sa_family_t.h
Home |
Main Index |
Thread Index |
Old Index