- /** Specifies a uninterpreted function with num_args parameters, a
- return value of numbytesretval bytes that returned the actual
- value val. The MCIDs for all inputs are then specified
- afterwards. The return MCID is MCID corresponding to the output
- of the uninterpreted function. Uninterpreted functions
- specified via this annotation are unique to the given dynamic
- instance. For example, if there is an unintepreted function
- call in a loop annotated by MC2_function, results from the first
- iteration will NOT be aggregated with results from later
- iterations.
- */
-
+ /** Tells MC2 that we just computed something that MC2 should treat
+ * as an uninterpreted function. The uninterpreted function takes
+ * num_args parameters and produces a return value of
+ * numbytesretval bytes; the actual return value is val. The
+ * following varargs parameters supply MCIDs for inputs. MC2
+ * returns an MCID for the return value of the uninterpreted
+ * function.
+ *
+ * Uninterpreted functions annotated with MC2_function are unique
+ * to the given dynamic instance. That is, for an unintepreted
+ * function call annotated by MC2_function which lives inside a
+ * loop, results from the first iteration will NOT be aggregated
+ * with results from subsequent iterations. */