38230ed9f7
-! 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.
7 lines
413 B
Text
7 lines
413 B
Text
$NetBSD: distinfo,v 1.4 2012/10/08 15:28:04 jaapb Exp $
|
|
|
|
SHA1 (frama-c-Oxygen-20120901.tar.gz) = 65aef0a88b788d11a6b5061dc08741492859de40
|
|
RMD160 (frama-c-Oxygen-20120901.tar.gz) = 76daf11770a52b1b1bc59ca9c576208ac08755a8
|
|
Size (frama-c-Oxygen-20120901.tar.gz) = 10815011 bytes
|
|
SHA1 (patch-Makefile) = f851797e599f682c4067fb02543b66c38cbd3446
|
|
SHA1 (patch-src_wp_Makefile) = bce0f55bae0718df462b2e1b6da689a4a00113d1
|