search

GaloisInc / pate

Patches Assured up to Trace Equivalence
Other
15 stars 2 forks source link

Support simple symbolic constraints in trace constraints format #436

Open danmatichuk opened 1 month ago

danmatichuk commented 1 month ago

Currently the JSON formatting for constraints only supports symbolic identifiers, which are difficult to test programmatically since they are fairly unstable. For the purposes of testing it would be convenient if simple expressions could be passed to identify variables for constraints: e.g. write read_mem(0xdeadbeef) rather than trying to guess its symbolic identifier. This would not need to be a complete expression parser, but would only need to be sufficient to handle some cases in order to facilitate testing.

danmatichuk commented 1 month ago

See failing PR #432 for why this is needed