OCM: Data Deep Comparison Equivalence

[Yiannis128]

Overhaul the partial equivalence mode to account for pointers.

• Primitives should check for equivalence like so:
  • Primitives that are a value: a == b
  • Pointers should be dereferenced: *a == *b.
  • Arrays should be dereferenced on every element: a[x] == b[x] where x = range(len(a)) and len(a) == len(b)
• Structures should check if both are null or not.
• Structures should individually check their elements like so:
  • If the element is a primitive, then treat with the above rules.
  • If the element is another structure, then compare elements.

The following proposal can be implemented using an ESBMC C Script (with the ClangAST backend and ESBMCCodeGenerator).

There are limitations to checking arrays all using this same method.

For more information, see this wiki page.

[Yiannis128]

OCM is planned to be removed from master pending more research. This was ambitious, perhaps, too ambitious.