Your first check

This tutorial starts with one C file. You need a working WeaveC installation.

Find a lifetime bug

Save this as example.c:

use-after-free.c

#include <stdlib.h>

struct node {
  int value;
};

static void node_free(struct node *n) {
  free(n);
}

int read_node(struct node *n) {
  struct node *alias = n;
  node_free(alias);
  return n->value;
}

Run the analyzer. The -- separator introduces flags for Clang:

weavec example.c -- -std=c17

The command fails with [weavec::use-after-free]. The diagnostic identifies the read of n->value, and its note points to the earlier release through alias.

There are two pointer variables, but they refer to the same object. node_free(alias) invalidates the object that n also names. WeaveC infers the helper’s release behavior from its body.

Fix the lifetime

Read the value before releasing its storage:

fixed.c

#include <stdlib.h>

struct node {
  int value;
};

static void node_free(struct node *n) {
  free(n);
}

int read_node(struct node *n) {
  int value = n->value;
  node_free(n);
  return value;
}

Replace the original contents with this version and rerun the command. Ordinary analysis succeeds. The function still consumes its input; callers must not use their pointer after the call.

Try checked safety

Ordinary analysis finds bugs, but a clean run is not a complete safety result. To require a supported function’s obligations to be discharged, use checked mode.

Save this as checked.c:

checked.c

int get(unsigned index) {
  int values[4] = {10, 20, 30, 40};
  if (index >= 4)
    return 0;
  return values[index];
}

weavec --checked-function=get --checked-report=safety.json checked.c -- -std=c17

The guard establishes that the index is within the initialized array on every path reaching the read. The selected check succeeds and writes a report.

Remove the guard and rerun it. The unknown index now leaves a bounds obligation unresolved; checked mode must reject that incomplete proof. It need not claim that every call will actually go out of bounds.

Continue

• Read the report to understand entry requirements and trusted operations.
• Integrate your build to use real include paths and defines.
• Look up a diagnostic for its meaning and resolution.