From 7bd10d9157220e7eebfbb67c3c3f12ad2a9deb97 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 18 Sep 2012 16:35:46 -0700 Subject: [PATCH] model: document behavior of ModelChecker::initialize_curr_action --- model.cc | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/model.cc b/model.cc index a13ccb7d..ebadbb6c 100644 --- a/model.cc +++ b/model.cc @@ -333,6 +333,17 @@ bool ModelChecker::process_write(ModelAction *curr) return updated_mod_order || updated_promises; } +/** + * Initialize the current action by performing one or more of the following + * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward + * in the NodeStack, manipulating backtracking sets, allocating and + * initializing clock vectors, and computing the promises to fulfill. + * + * @param curr The current action, as passed from the user context; may be + * freed/invalidated after the execution of this function + * @return The current action, as processed by the ModelChecker. Is only the + * same as the parameter @a curr if this is a newly-explored action. + */ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) { ModelAction *newcurr; -- 2.34.1