Support conditional compilation (`#[cfg]`) in Anneal verification targets

[joshlf]

Problem

Anneal currently ignores #[cfg(...)] attributes during its AST scan. It parses all items syntactically, regardless of whether they are enabled for the current build target.

If a user annotates an item that is conditionally compiled out (e.g., a function guarded by #[cfg(windows)] when running on Linux, or an item requiring a disabled feature), Anneal still identifies it as a verification target. It then invokes charon, which performs a real compilation (cargo check). Since the item does not exist in the compiled artifact, Charon crashes or fails with an "Item not found" error.

Goal

Anneal should simulate rustc's conditional compilation logic during the parsing phase. If an item is disabled by the current configuration, Anneal should ignore it entirely: neither extracting it as a target nor traversing into it (in the case of modules).

Proposed Solutions

Solution A: Copy all files; don't bail on missing files

We just need it to be the case that, if a project would have failed to compile normally, then its shadow copy will fail to compile; and if it would have succeeded, then its shadow copy will succeed.

Thus, given a mod foo; declaration, we can simply attempt to find a corresponding foo.rs or foo/mod.rs and copy it. If we succeed and mod foo; ends up being cfg'd out, then the file is ignored in the subsequent build, which is fine. If we fail and mod foo; is not cfg'd out, then compiling the original source would have failed too, and so it's fine that the shadow crate fails to compile.

It's an open question whether this works with conditional paths. I _think_we can apply the same approach (copy all files we find names for, but fail silently), and the same logic applies for why it's fine, but I'd need to think harder about it.

#[cfg_attr(a, path = "foo_a.rs")]
#[cfg_attr(b, path = "foo_b.rs")]
mod foo;

Solution B: Evaluate cfgs

We should implement a evaluate cfgs using the cfg-expr crate.

##$## Context gathering

We need to capture the build context to evaluate cfg predicates:

• Invoke rustc --print cfg to obtain the global target key-value pairs (e.g., target_os = "linux", unix, target_pointer_width = "64").
• Extract the list of enabled features for each package from the cargo metadata resolution graph.

###$# Conditional parsing

Update the AnnealVisitor (src/parse.rs) to check for #[cfg] attributes before processing any item:

1. When visiting an item (Fn, Mod, Impl, etc.), parse any #[cfg(...)] attributes using cfg-expr.
2. Check the predicate against the gathered context (Target CFG + Package Features).
3. Then:

• If false: Skip the item completely. Do not extract annotations and do not descend into children.
• If true: Proceed as normal.

##$## Module resolution

This logic must crucially apply to mod foo; declarations. If a module is #[cfg(false)], Anneal must not attempt to resolve the file path or parse the file, avoiding "File not found" errors for platform-specific modules.