Skip to content

Use LazyEval instead of Lazy in C2PODomain.#1717

Merged
jerhard merged 4 commits into
masterfrom
c2po-fix-lazy
Mar 26, 2025
Merged

Use LazyEval instead of Lazy in C2PODomain.#1717
jerhard merged 4 commits into
masterfrom
c2po-fix-lazy

Conversation

@jerhard
Copy link
Copy Markdown
Member

@jerhard jerhard commented Mar 25, 2025

This PR fixes the CI failures for marshalling tests that occur with C2PO in the ulocked pipeline.

The failure of the marshalling tests for C2PO is due to the normal form that appears as part of the domain of C2PO, being Lazy.t. Thus, these normal forms are of a functional value that cannot be marshaled.

This PR changes this by using LazyEval in place of Lazy. Then, the input data for the computation of the normal form --- the other record entries of the domain --- are kept instead of a closure capturing these values. The eval that is defined then performs the evaluation of the normal form.

@sim642 sim642 self-requested a review March 25, 2025 20:53
@sim642 sim642 added testing relational Relational analyses (Apron, affeq, lin2var) labels Mar 26, 2025
@sim642 sim642 added this to the v2.6.0 milestone Mar 26, 2025
Comment thread src/cdomains/congruenceClosure.ml Outdated
@jerhard jerhard merged commit f99a9f6 into master Mar 26, 2025
@jerhard jerhard deleted the c2po-fix-lazy branch March 26, 2025 14:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

relational Relational analyses (Apron, affeq, lin2var) testing

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants