crabllvm (seahorn/crab-llvm) is incompatible with LLVM 16 — `--add-invariants` is a no-op

[GuilhermeBn198]

Summary

The --add-invariants flag (which adds program invariants via Crab-LLVM) is a no-op in the current build because the Crab-LLVM binary is never built.

Root cause

• cmake/FindCrabLlvm.cmake uses ExternalProject_Add to pull seahorn/crab-llvm, but this module is never included by the modern CMakeLists.txt (LLVM 16 / New PM era).
• seahorn/crab-llvm is a legacy SeaHorn dependency tied to LLVM 6–12 and is not compatible with LLVM 16.
• modules/frontend/caller.cpp compileToCrabLlvm() invokes ${MAP2CHECK_PATH}/bin/crabllvm/bin/crabllvm.py, which does not exist in any produced install layout.

Current workaround (landed)

modules/frontend/map2check.cpp now detects the absence of bin/crabllvm/bin/crabllvm.py and falls back to plain compilation with a warning, instead of breaking the pipeline (fix: fall back to plain compile when crabllvm is not built).

Desired outcome (future)

Either:

1. Build crab-llvm against LLVM 16 (if upstream supports it), wiring FindCrabLlvm.cmake into the modern build and installing the binary so --add-invariants works again; or
2. Drop the feature: remove --add-invariants, compileToCrabLlvm(), and FindCrabLlvm.cmake from the codebase, and update the docs (docs/map2check_migration_plan.md mentions Crab-LLVM as "presente mas não ativo").

Context

--add-invariants was used as a pass-2 fallback in the CASTLE/Juliet baseline evaluation; it is currently skipped because of this gap. Related: modules/frontend/caller.cpp compileToCrabLlvm().

[github-actions]

Welcome to the Map2Check! We are excited that this is your first issue!