minor issues

harmonylang · Aug 19, 2023 · b8efdd2 · b8efdd2
1 parent 92488d1
commit b8efdd2
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/harmony_model_checker/charm/charm.c b/harmony_model_checker/charm/charm.c
@@ -415,7 +415,6 @@ unsigned int check_finals(struct global *global, struct state *state, struct ste
 
  // Check each finally predicate
  for (unsigned int i = 0; i < global->nfinals; i++) {
- assert(step->ctx->sp == 0);
  assert(!step->ctx->failed);
  // step->ctx->terminated = false;
  // ctx_failure(step->ctx) = 0;

diff --git a/harmony_model_checker/charm/graph.h b/harmony_model_checker/charm/graph.h
@@ -54,7 +54,7 @@ struct edge {
  struct node *dst; // destination node
  hvalue_t after; // resulting context (TODO. index in dst context bag)
  struct access_info *ai; // to detect data races
- uint16_t inv; // pc of invariant
+ int16_t inv;  // pc of invariant (negative if finally clause)
  uint16_t nsteps; // # microsteps
  uint8_t ctx_index; // index of context in src state context bag
  bool interrupt : 1; // set if state change is an interrupt