[CN-Exec] Do not inject synthesized terms

[peterohanley-galois]

The injection model breaks down for ++a; because the ++ part should just disappear but the previous handling doesn't know that. From what I've determined only ++a and --a actually break the (wrongly assumed) invariant that the members of an AIL term have locations that actually represent their source position. #39 fails in the same way as processing ++a but I don't think it's from the same cause. This needs rems-project/cerberus#950 as its cerberus.

[rbanerjee20]

Looks good to me, subject to rebasing

[rbanerjee20]

Would you mind updating the cn.opam file with the correct commit hash for Cerberus? i.e. 6e3e8be

[peterohanley-galois]

I ran the checks on the Galois version of this repo and I got two parsing failures, but I haven't made any parsing changes

[peterohanley-galois]

This is the fix for #80

[rbanerjee20]

I ran the checks on the Galois version of this repo and I got two parsing failures, but I haven't made any parsing changes

Perhaps an out-of-date Cerberus version? If you change the cn.opam file locally and then reinstall cerberus-lib through opam, it might work

[peterohanley-galois]

Perhaps an out-of-date Cerberus version? If you change the cn.opam file locally and then reinstall cerberus-lib through opam, it might work

I was running the CI.

[peterohanley-galois]

It was actually that the parse state number in the recorded error message had changed, and those aren't canonicalized in the recorded files.

[peterohanley-galois]

CI passed in our local branch, please let this run and then we can merge it.

[rbanerjee20]

Sure, please rebase on main and then I'll run them

[rbanerjee20]

spec testing CI seems to be failing (an unexpected pass of something that's supposed to fail). I'm just rerunning it to make sure it's not a random failure (which happens occasionally in CN-test-gen) and then I'll try it out locally

[ZippeyKeys12]

Not cn-test-gen, it's #96

[rbanerjee20]

@peterohanley-galois if you could rebase again I'll merge it as soon as the checks pass

[peterohanley-galois]

@peterohanley-galois if you could rebase again I'll merge it as soon as the checks pass

@rbanerjee20
Ok please run the tests and hopefully this can get in before another patch lands on main.

[rbanerjee20]

@peterohanley-galois sorry, same thing once again. Something new got merged in

In the future, I could rebase and push on your branch directly if there are no conflicts - would save both of us time. If there are conflicts I can leave it to you. Also happy to leave it to you in general

[rbanerjee20]

In the future, I could rebase and push on your branch directly if there are no conflicts - would save both of us time. If there are conflicts I can leave it to you. Also happy to leave it to you in general

It seems that I don't have permission to push to the Galois fork, otherwise I'd have been happy to. Could someone else with the correct permissions take over this PR now? (e.g. @ZippeyKeys12 if you have a minute). I'm going to log off now

[ZippeyKeys12]

Did you uncheck "allow edits by maintainers"? That's what allows us to rebase for you... @peterohanley-galois

To get this merged, I just remade the PR.