Changes between Version 2 and Version 3 of Comparison

Timestamp:

03/21/14 15:19:15 (12 years ago)

Author:

zirkel

Comment:

--

Comparison

@@ -24 +24 @@
         v. Spawn statements for spec and impl
         vi. Wait statements for spec and impl
-        vii. Assertions checking equality of each pair of output variables. e.g. suppose `x` is an output variable.  If the variables are renamed `x_spec` and `x_impl`, an assertion `$assert(x_spec==x_impl);` will be added.  Maybe we need to have a flag indicating that this assertion is special and can read output variables without error?  Or, make a system function for comparing output variables that doesn't have this restriction and can directly compare symbolic expressions for arrays, etc.
+        vii. Assertions checking equality of each pair of output variables. e.g. suppose `x` is an output variable.  If the variables are renamed `x_spec` and `x_impl`, an assertion `$assert(x_spec==x_impl);` will be added.  Maybe we need to have a flag indicating that this assertion is special and can read output variables without error?  Or, make a system function for comparing output variables that doesn't have this restriction and can directly compare symbolic expressions for arrays, etc.  Something like `$equals(void *, void *)`. The system function will evaluate each pointer, dereference, form a reasoner from the path condition, check equivalence of expressions. Could return void or bool.  Log error if they disagree.