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