docs: compatibility matrix, semantic deltas and release packaging (#5)

.github/workflows/CI.yml

@@ -120,6 +120,9 @@ jobs:
           done
           [ "$ok" = 1 ]
 
+      - name: Testar empacotamento de release (header, bibliotecas e docs)
+        run: scripts/test-package-release.sh
+
       - name: Checar segurança de dependências (cargo-deny)
         uses: EmbarkStudios/cargo-deny-action@v2
         with:

.gitignore

@@ -17,3 +17,6 @@ tarpaulin-report.html
 
 # Header C gerado por cbindgen
 map2check.h
+
+# Arquivos de release (scripts/package-release.sh)
+dist/

CHANGELOG.md

@@ -0,0 +1,61 @@
+# Changelog
+
+All notable changes to `map2check-library` are recorded here. The format
+follows [Keep a Changelog](https://keepachangelog.com/en/1.1.0/), and
+versions follow [Semantic Versioning](https://semver.org/). The version
+comes from `Cargo.toml` and is repeated in `MAP2CHECK_VERSION`
+(`include/map2check.h`) and in the `Dockerfile` label.
+`tests/header_version.rs` fails when this file has no section for the
+current version.
+
+Compatibility with the legacy C library is tracked in
+[`docs/api-deltas.md`](docs/api-deltas.md) and
+[`docs/semantic-deltas.md`](docs/semantic-deltas.md); a change that touches
+the C ABI or the JSON report must update them.
+
+## [Unreleased]
+
+### Added
+
+- `docs/api-deltas.md` symbol/signature matrix for the core C API and the
+  Map2Check passes, and `docs/semantic-deltas.md` with reproducible
+  behaviour differences, both checked by `tests/compat_docs.rs` (#5).
+- `docs/integration-guide.md` and `docs/release.md`;
+  `scripts/package-release.sh` builds the release archive with the C
+  header, both static libraries and the docs (#5).
+
+## [1.0.0-rc1] - Unreleased
+
+First release candidate of the Rust rewrite (milestones M1–M3).
+
+### Added
+
+- Rust implementation of the C ABI in `rust/src/ffi.rs`, with
+  `include/map2check.h` generated by `cbindgen` from `build.rs`.
+- `map2check_reset()`, `get_next_step()`,
+  `map2check_map_non_static_alloca`, `map2check_map_funct_address`,
+  `map2check_check_free_resolved_address`, and the LibFuzzer generators
+  `__VERIFIER_nondet_*`, `__VERIFIER_assume`, `__VERIFIER_assert`,
+  `__VERIFIER_error` and `map2check_fuzzer_assume` (feature `libfuzzer`)
+  (#2, #3).
+- `#define MAP2CHECK_VERSION` in the generated header (#28).
+- Unit tests for every exported FFI symbol and a checklist that fails on an
+  untested export (#29).
+- CI: formatting, Clippy, tests, an ASan/UBSan C harness, C integration
+  programs, cargo-deny, cargo-audit, Docker build, and an 80% coverage gate
+  outside `ffi*.rs` (#1, #30); branch protection for `feature/rust` and
+  `master` (#26).
+
+### Changed
+
+- JSON report produced by `serde_json`; shape in
+  `docs/integration-guide.md`, differences in SD-01.
+- `map2check_save_nondet_log_char` takes `char` as `i8` (see
+  `docs/api-deltas.md`).
+- Every export catches panics at the FFI boundary, and the global state
+  sits behind a mutex (#2).
+
+### Removed
+
+- `map2check_gen_data_fuzzer_*`, `next_current_step` and the C-era build
+  files and docs (#27). See `docs/api-deltas.md` for each removal.

README.md

@@ -156,32 +156,22 @@ Map2Check Tool (LLVM Pass / Instrumentação)
 
 ## Output JSON
 
-Ao final da análise, `print_all_containers_as_json()` emite no stdout:
-
-```json
-{
-  "map2check_log": {
-    "result": "true",
-    "property": "NONE",
-    "step": 42,
-    "line": 0,
-    "function_name": "",
-    "Container_NonDetLog": [
-      {
-        "step": 1,
-        "line": 10,
-        "scope": 0,
-        "function_name": "main",
-        "value": { "type": "INT", "value": 7 }
-      }
-    ],
-    "Container_TrackBBLog": [ ... ],
-    "Container_AllocationLog": [ ... ]
-  }
-}
-```
+Ao final da análise, `print_all_containers_as_json()` emite no stdout um objeto `map2check_log` com o veredito (`result`: `"TRUE"`/`"FALSE"`), a propriedade violada e os containers `Container_TrackBBLog`, `Container_NonDetLog` e, só em violações de memória, `Container_AllocationLog`. O formato exato, com exemplos verificados contra o serializador, está em [`docs/integration-guide.md`](docs/integration-guide.md#json-report).
+
+## Compatibilidade e releases
+
+- [`docs/api-deltas.md`](docs/api-deltas.md): matriz de símbolos e assinaturas da API C (núcleo e passes do Map2Check) em relação ao C legado.
+- [`docs/semantic-deltas.md`](docs/semantic-deltas.md): diferenças de comportamento, cada uma com caso reproduzível e teste.
+- [`docs/integration-guide.md`](docs/integration-guide.md): como linkar `libmap2check.a`, ordem de chamadas e formato do relatório JSON.
+- [`docs/release.md`](docs/release.md) e [`CHANGELOG.md`](CHANGELOG.md): processo de release e histórico de versões.
+
+`tests/compat_docs.rs` falha em três casos: quando um export do header não está na matriz (ou está com a declaração errada), quando um `SD-NN` aponta para um teste que não existe e quando os exemplos JSON do guia divergem da saída real. Toda mudança na ABI C ou no relatório JSON atualiza esses documentos no mesmo PR.
 
-`Container_AllocationLog` só é incluído quando a violação é de segurança de memória (`MemsafetyFree`, `MemsafetyDeref`, `MemsafetyMemcleanup`).
+Para montar o pacote de release localmente:
+
+```sh
+scripts/package-release.sh   # dist/map2check-library-<versão>-<alvo>.tar.gz + SHA256SUMS
+```
 
 ## Map2Check flow com a biblioteca