search

c4-project / c4f

The C4 Concurrent C Fuzzer
MIT License
14 stars 1 forks source link

Propagate postcondition of C/Litmus file through litmusifier #61

Closed MattWindsor91 closed 4 years ago

MattWindsor91 commented 5 years ago

When we have a C/Litmus file that we're delitmusifying, we should be able to strip out its postcondition, carry it through to when we're building the assembly litmus test for it, and attach it (with variable redirection as necessary). This will be a big step towards postcondition-based testing (as opposed to full simulation on both sides and set comparison).

This likely interacts with #60, as we'll need to send the postcondition down the pipeline.

MattWindsor91 commented 4 years ago

Closing this as it seems that aux.json combined with the fact that we no longer sanitise/litmusify satisfies this requirement