[This file was autogenerated by LPdoc, please do not edit.] This documentation corresponds to version 1.5 (2022/3/2, 20:34:30 CET). CiaoPP ****** CHANGELOG_CIAOPP **************** Version/Change Log ================== Version 1.5 (2022/3/2, 20:34:30 CET) * ADDED: CiaoPP is included now by default with the 'devenv' bundle. * ADDED: Output options in the 'output/2' predicate. * ADDED: More examples (most of them for verifly). * ADDED: Documentation for debugging analyses. * ADDED: 'ciaoppcl' can start as an active module (flycheck). * IMPROVED: Better automatic selection of analysis domains (covering better the properties to be checked; using mode domains before type domains, etc.); 'dom_sel' flag to decide whether to automatically select domains for verification. * IMPROVED: Refactoring and improving 'ctchecks' (compile-time assertion checking) code: modular ctchecking working again (i.e., after intermodular fixpoint); report assertions per module; better messages; many bug fixes. * IMPROVED: Reducing boilerplate code in the implementation of analysis domains using the new 'aidomain' package. * IMPROVED: Simplified menu, unified menu for analysis and ctchecks. * IMPROVED: Improved precision of (nf,det) analysis domains. Adding (experimental) new 'nfdet' combined analysis domain. * CHANGED: Change default setting for entry point selection from assertions (exported calls by default). * CHANGED: Disabled output for 'ciaoppcl -V'. * CHANGED: Assertion simplification (eliminating statically proven properties from run-time checks) now enabled by default during assertion checking. * CHANGED: 'trust pred' assertions expanded to 'check calls', 'trust success' and 'trust comp' assertions. * CHANGED: Abort 'auto_interface' action early if there is a compilation error. * CHANGED: 'pp_info' flag (printing analysis infor at literal level) moved to the naive menu. * FIXED: Many bug fixes and performance improvements: eliminated some dangling choicepoints; avoid printing some calls assertions twice; wrong use of 'denorm_goal_prop/3' changed to 'prop_unapply/3'; missing clause to 'abs_exec_cond:type_of/4' to handle 'deftypes' domain. * FIXED: Bug in treatment of dynamic predicates. Version 1.4 (2020/11/18, 6:18:7 CET) * General changes and new features: * LLVM-based frontend improved and moved to its own bundle (see 'ciaopp_llvm' bundle). * Split 'typeslib' as a separate bundle. * Allow heads of entry assertions to be non-normalized. * Adapted to new hiord. * [new] Command 'ciaopp-dump', which performs several actions over a ciaopp analysis dump: it subsumes the old 'ciaopp-dump-cmp' and 'ciaopp-dump-cmp' commands. New options for: showing the contents of a dump file, a code reachability report, static, offline checks of assertions using a dump file, and general statistics for the analysis results. * [new] Added '-op Suffix' option to ciaopp command-line (useful for flycheck). * [new] Warning if no entries were found * [new] Unified messages, now controlled by 'ciaopp_log.pl' * [new] 'ciaopp-batch' command to run ciaopp on many files and with timeouts. * [new] Modular (non-incremental) analysis with types (shortening). * [new] Bottom-up incremental update of fixpoint (at literal level). * [new] Modular (non-incremental) analysis with types (shortening). * Domains: * Implemented domains using (a special) trait package. * Added 'needs/2' operation. * Renamed 'abstypes_abs' to 'auxinfo_asub'. * eterms: 'member/2', '=/2' as native properties (for assertions). * pdb: * Optimize 'pdb_compute_lub': top if any 'ASub' is top. * Use 'fail' literals. * sharing: fixed 'free/1' handlers * shfr: fixes in handlers of '==/2', '=/2', ''\=='/2', ''\='/2', 'free/1' (native version of 'var/1') * Fixpoints: * Split compilation options ('debug', 'trace', 'rtchecks') in common file 'fixpoint_options.pl' * Improved tracing of clauses * Refactored fixpoints to make them easier to merge * Fixpoint 'dd': * [fix] Reuse a complete with the same head but different vars order * [performance] Using get_memo_table because Id+Key is unique * [fix] Case in which a literal is not reachable * Improved documentation * Analysis of higher-order code: * [new] Flag for automatic generation of entries of meta calls. * [fix] 'call/N' was not being detected as meta predicate (and flattened when possible). * [new] '\+' not treated as meta, flatten calls known at compile time. * Flags and options menu: * [new] Flag to remove useless (unreachable) completes after fixpo. * 'punit_boundary': change default value to bundle. * Included 'incanal' flag, changed 'ext_policy' in menu (same as 'pp_flag'). * Improved options menu (added and simplified dependencies, simplified text, grouped actions, better documentation). Version 1.3 (2019/11/3, 11:16:23 CEST) * New functionality: * Backported (and improved) incremental analysis (incanal) from CiaoPP 0.8. * Integrated incremental and modular analysis ('pp_flag incremental=on') * Integrated modular analysis in the general analysis driver. * Added analysis using run-time semantics of assertions to the 'dd' fixpoint ('pp_flag' 'old_trusts=off'). * Fixes in meta-calls (work in progress). * Modularized domains, now they use the aidomain package (work in progress). * Added generic, non relational domain with simpler domain operations. * New flag value: restrict modular analysis to the modules of a bundle ('pp_flag' 'punit_boundary=bundle'). * Performance improvements: * Added hook to cache library assertions. * Added flag to load modules faster by preloading ciao libraries. * Fixed many dangling choicepoints across all modules. * Fixed performance issues in modular analysis. * Fixed bug of metacalls inside a recursion ('dd' fixpoint). * User interface and documentation: * Rearranged manual. * Created web interface for demos (see 'ciaopp_online' bundle). * Added a high level interface for intermental analisis (incanal). * Benchmarks, internal testing, and debugging: * Tests/benchmarks moved to a separate bundle (ciaopp_tests). * Added tests for gitlab CI (continuous integration). * Some fixes in the davinci interface. * Fixed (documentation) assertions. CiaoPP can be run with the package rtchecks. * Added analysis_stats.pl to unify statistics collecting. * ciaopp-dump-cmp: new command to compare two ciaopp analaysis dumps. * ciaopp-dump-fmt: new command that outputs the analysis in dot format. * New flag value: Raw analysis printer ('pp_flag' 'output_lang=raw'). * Added 'pp_flag' to trace fixpoints. * Other bug fixes, cleanups, refactoring, etc.: * Removed 'api' (now using 'p_unit'). * Fixed maintaining 'plai_db' for complete operations * Fixed classifying mistakenly recursive predicates as non recursive (meta predicates). * Fixed issue with reexported predicates in p_unit. * Fixed problem with meta_predicates that did not have any meta argument. * Added 'free/1' to 'sharefree_clique' domain. * Replaced 'runtime_control:statistics/2' by 'analysis_stats:pp_statistics/2'. * Using 'p_unit/program_keys.pl' for the keys of ciaopp. Version 1.2 (2006/1/3, 11:16:23 CEST) Check point Version 1.0 (2001/11/7, 19:5:57 CET) Major code reorganization from CiaoPP 0.8. Moved to repo system. See 0.8 manual for changelog prior to 1.0 (covers 1999-2000).