CHANGELOG (p.mopsa.1.2.doc.CHANGELOG)

1.2

High-level changes:

Sound support of bitfields

Add bitmask abstract domain

Property-based testing for non-relational numeric abstractions

Build system is simplified and now relies on dune's include_subdirs qualified option

Warn about usage of prototype domains through runtime warnings and in the analysis report

Detailed changelog:

!298 by @rmonat: pre-release fixes (CHANGELOG.md, ...)

!296 by @antoine_mine: C, extended locations to track C macro expansions

!239, !303 by @rmonat: experimental heterogeneous relational domain

!285 by @rmonat: extend log hooks to allow displaying only original exprs/stmts

!302 by @antoine_mine: fix for old clang version (10) in C frontend

!300, !301 by @rmonat: fix Python's except semantics

!237 by @Mm72: fix argument clash in function call

!299 by @antoine_mine: fix compilation error on CLang 14

!246 by @aouadjaout/@rmonat: transform bitfields into bitwise operations

!297 by @rmonat: ci, fix interactive engine test

!295 by @antoine_mine: C source printing prints global variable declarations before simplification

!294 by @antoine_mine: parser fixes to analyze coreutils 9.7

!289 by @Mm72: fix typo in file descriptor's table

!290 by @rmonat: fix bwd_round in floating point interval domain

!288 by @rmonat: enable sudo in docker images

!287 by @rmonat: fix widening delay

!286 by @rmonat: ensure file is closed even during parsing errors

!275, !284 by @rmonat: dune, use include_subdirs qualified

!278 by @rmonat: add collecting semantics domain for P(V->Z)

!282, !292 by @rmonat: warn about prototype analyses

!283 by @antoine_mine: opam depexts: fix clang package name in Gentoo

!264 by @aouadjaoutt/@rmonat: add the domain of bitmasks

!274 by @rmonat: relational: avoid double call to mopsa_to_apron_var

!277 by @rmonat: add option to disable wraparound semantics for signed integer overflow

!280 by @Mm72: tag synthetic expressions/statements from original ones

!281 by @Mm72: fix usage help for relational overflow check flag

!276 by @rmonat: python, fix parser in cases such as a = b = c = [1, 2]

!270 by @rmonat: implement notion of "control context", generalizing callstacks

!271 by @Mm72: document the process of creating output files for manual

!269, !272 by @Mm72: property-based testing for non-relational integer domains

!268 by @antoine_mine: add support for Clang 20 frontend

1.1

Release 1.1 brings several expressivity, precision and interface improvements, notably:

Trace and state partitioning. :warning: introduces breaking changes in the API of domains.

Suggestions to trigger automatic testcase reduction whenever Mopsa crashes

As a side-effect, Mopsa is able to generate preprocessed files from make targets using option -c-preprocess-and-exit=file.i, which might be useful for other users too! This has been experimented on our coreutils benchmarks, and can also be used to generate the preprocessed files used in the Software-Verification Benchmarks

Bash completion support, thanks to arg-complete developped by Simmo Saan.

Detailed changelog:

!241 by @rmonat: pre-release fixes (CHANGELOG.md, ...)

!265 by @rmonat: bash completion support

!266 by @rmonat: ci fix

!144 by @rmonat: leveraging creduce/cvise testcase reduction for Mopsa

!240 by @rmonat + @aouadjaout: remove post_to_flow in stubs

!253 by @rmonat: state partitioning improvements

!260 by @antoine_mine: mopsadb: remember object files for target, prints absolute path for objects in libraries

!250 by @rmonat: fix #206 (panic: pointers do not point to the same type)

!259 by @aouadjaout: simplify initializers of global and static variables in C

!261 by @antoine_mine: fix for #211 (Inline assembly parsing messes $ and % symbols)

!255 by @rmonat: fix #204 (Static packing does not take into account integers within structs)

!257 by @jboillot: add usage of already implemented abstract transfer functions in congruence domain

!249 bv @rmonat: fix #202 (not_found triggered by string length domain )

!254 by @rmonat: fix #200 (panic catches in interactive engine) + #205 (engine stack overflow)

!256 by @rmonat: update output of checks to ensure consistency of displayed results

!248 by @rmonat: fix issue #85 (Not_found raised on ill-behaved program)

!258 by @aouadjaout: rename effect to change (for OCaml 5.3 compat)

!180 by @antoine_mine: only abort parsing for fatal Clang errors, not regular errors (nor warnings)

!251 by @aouadjaout and @rmonat: fix #208 (Bad interaction between state and trace partitioning)

!252 by @aouadjaout and @rmonat: Cells: remove call to post_to_flow in expand to keep offset constraints in the effects

!235 by @rmonat: various fixes for lipari tutorial

!150 by @antoine_mine: translate unknown builtins to a specific AST node instead of aborting

!247 by @rmonat: CI fixes (mopsa-diff; no manual confirmation of CI job downstream-benchmarks)

!245 by @aouadjaout: fix the printing of partitioning

!244 by @antoine_mine: support for Clang 19 as C frontend

!243 by @antoine_mine: hardcoded no-warning-as-error for incompatible function pointer types

!242 by @aouadjaout: fix broken CPython CI after merging partitioning

!130 by @aouadjaout: introduces partitioning in Mopsa :warning: Breaking changes, cf. https://gitlab.com/mopsa/mopsa-analyzer/-/merge_requests/130#breaking-changes

!236 by @Mm72: fix range of sub-expressions of binary operators in universal

!234 by @edwintorok: fixes in mopsa-build (handling of -Wl,-E)

1.0

This is the initial version of Mopsa. See the README.md to know more about Mopsa.

Latest improvements:

!229 by @rmonat: last pre-release fixes to README, opam file, etc

!232 by @antoine_mine: update mopsa-build docker image to Ubuntu 24.04 LTS

!231, !233 by @rmonat: fix header files of multilanguage stubs, required for newer versions of Clang

!216 by @jboillot: improve the precision of the backward wrap operator for integer intervals

!221 by @rmonat: display selectivity of all analyses, and count safe pointer checks in C

!230 by @antoine_mine: asm statements are parsed, and soundness assumptions are raised whenever those statements are encountered during an analysis.

!218 by @rmonat: improvements to interactive engine (command chaining through ;, exit, documentation)

!217 by @jboillot: improve symbolic rewriting domain (support of ~, constant propagation, improve support of ToBeKSplit)

!209 by @antoine_mine: fix for forward/backward modulo operator in congruences

!228 by @antoine_mine: provide external clang dependencies in mopsa.opam

!226 by @rmonat: pre-release fixes (removed zlib, fix in release script, improvement of README)

!225 by @mm72: fix targets check in simplifed produce combiner

!214 by @rmonat: update minimum requirements

!220 by @rmonat: fix excluded powerset case when division is not exact

!215 by @jboillot: correct the semantics of shift-right to match what is done in other domains (division by 2^lhs but rounded towards -oo, rather than rounding to 0 provided by C integer division)