86 Getting started with proven

86.1 The choice of having nothing to install

proven has no installation procedure. Compile the source you have obtained together with your program and that is all. The source ships inside this book’s repository, github.com/rubidus-api/proven_c_book, under vendor/proven/. There are only two directories that matter.

• src/proven/ — the portable body. The operating system is not called here.
• platform/ — a thin layer that makes system calls. It is the only part that must be changed when moving to a new machine.

In an environment with no operating system (embedded) it is built without platform/. This separation settled the shape of the whole library — the demand “it must run anywhere” becomes the discipline “keep neither hidden allocation nor hidden global state”.

86.2 How this book’s examples are built

To state it honestly, this book’s proven examples are compiled as follows. The library’s source is made into object files once and linked with the example.

$ cc -std=c23 -O1 -Ivendor/proven/include -c vendor/proven/src/proven/*.c
$ cc -std=c23 -Wall -Wextra -Werror -Ivendor/proven/include \
     hello.c vendor-obj/*.o -lm -o hello

The first line handles the body, the second my program. -I tells it where to find headers (chapter 54), -lm joins the mathematical functions. These two lines are what this book’s verification script really runs every time, and every execution result printed on these pages is the output of a program made that way.

86.3 The first program

One #include <proven.h> opens the whole library.

#include <proven.h>

int main(void)
{
    const char *name = "world";
    int         count = 3;
    double      ratio = 0.75;
    bool        ready = true;
    char        grade = 'A';

    /* {} is only a placeholder and has no type. The type comes from the argument */
    proven_println("Hello, {}! You have {} messages.",
                   PROVEN_ARG(name), PROVEN_ARG(count));

    /* whatever the type, it goes through the same placeholder */
    proven_println("ratio={} ready={} grade={}",
                   PROVEN_ARG(ratio), PROVEN_ARG(ready), PROVEN_ARG(grade));

    /* the format specification goes after the colon — width, alignment, digits */
    proven_println("|{:>8}|{:<8}|{:.3}|",
                   PROVEN_ARG(name), PROVEN_ARG(name), PROVEN_ARG(ratio));
    return 0;
}

Hello, world! You have 3 messages.
ratio=0.750000 ready=true grade=A
|   world|world   |0.750|

We read it line by line. proven_println takes a format and arguments and prints one line to standard output — so far the same as printf. What differs is the placeholder.

• {} has no type in it. It is neither %d nor %s but simply {}.
• The type comes from the argument. PROVEN_ARG(x) looks at x’s type and wraps the value with a fitting tag attached.
• So chapter 85′s third bug — the mismatch of format and argument — structurally cannot happen. The type is not written twice, so there is no place for them to go out of step.

What is written after the colon, as in {:>8}, corresponds to the width, alignment and precision seen in chapter 61. > is right alignment, < left alignment, .3 is to three decimal places. That the alignment symbol comes first is what differs from printf.

86.4 Three rules — the key to this whole part

The functions ahead number more than a hundred, but the rules for reading their signatures are only three. Get these three into your hand and you can read half of any function you have never seen, without the documentation.

1. Only a function that takes an allocator as an argument takes memory. If proven_allocator_t appears in the signature it means “this function may allocate”, and if it does not, it takes not one byte. So which functions are usable in embedded work and which are not divide before your eyes (chapter 89).
2. Failure comes as a value. If there is no result to return it gives a single proven_err_t; if there is, an {err, value} bundle. Before checking err you do not look at value (chapter 87).
3. Give a thing back with the allocator you made it with. What was obtained with _create is let go with _destroy, and what has view in its name is borrowed and is not destroyed (chapters 88 and 89).

The naming rules have almost no exceptions either.

86.5 The life of one object

Rather than reading three lines of rules, it is quicker to follow one real thing to the end. The program below holds the whole course of making, using and giving back a string object on one screen.

/* The first real program — the whole course of making an object, using it and
   giving it back. The skeleton of a proven program is all in this one file. */
#include <proven.h>

/* (1) Where does the memory come from — the caller decides (the allocator parameter).
   (2) Failure arrives as a value — value is not looked at before err is checked.
   (3) What was made is given back through the allocator it was made with. */
static proven_err_t build_line(proven_allocator_t alloc,
                               proven_u8str_view_t who,
                               int count,
                               proven_u8str_t *out)
{
    /* a string with room for 64 bytes, obtained from alloc */
    proven_result_u8str_t made = proven_u8str_create(alloc, 64);
    if (!proven_is_ok(made.err))
        return made.err;

    proven_u8str_t line = made.value;      /* taken out only after the check */

    /* Appended through a format. On failure the original is left untouched.
       Formatting returns, along with err, "bytes written / bytes needed" */
    proven_fmt_result_t r = proven_u8str_append_fmt(&line, "{} has {} message(s)",
                                                    PROVEN_ARG(who), PROVEN_ARG(count));
    if (!proven_is_ok(r.err)) {
        proven_u8str_destroy(alloc, &line); /* returned on the failure path too */
        return r.err;
    }

    *out = line;                            /* ownership passes to the caller */
    return PROVEN_OK;
}

int main(void)
{
    /* the heap allocator — standard malloc wrapped in the library's interface */
    proven_allocator_t alloc = proven_heap_allocator();

    proven_u8str_t line;
    proven_err_t e = build_line(alloc, PROVEN_LIT("alice"), 3, &line);
    if (!proven_is_ok(e)) {
        proven_println("build failed: {}", PROVEN_ARG((int)e));
        return 1;
    }

    /* an owned string -> a borrowed view. A view is valid only while the original lives */
    proven_u8str_view_t v = proven_u8str_as_view(&line);
    proven_println("line   = {}", PROVEN_ARG(v));
    proven_println("length = {} bytes", PROVEN_ARG(v.size));

    /* the meeting point with old APIs that need NUL termination (no copy, no allocation) */
    proven_println("as C string = {}", PROVEN_ARG(proven_u8str_as_cstr(&line)));

    proven_u8str_destroy(alloc, &line);     /* through the very allocator it was made with */

    /* Destroying empties the struct to zero — so it cannot point at the returned
       buffer again. Hence the length after destroying is 0, and the contract is
       that this object is not used any further. */
    proven_println("after destroy, length = {}",
                   PROVEN_ARG(proven_u8str_as_view(&line).size));
    return 0;
}

line   = alice has 3 message(s)
length = 22 bytes
as C string = alice has 3 message(s)
after destroy, length = 0

Six places to point at.

① It took an allocator as an argument. That build_line’s first argument is an allocator is the declaration that “this function may take memory”. The caller settles whether to give it the heap or an arena (chapter 89).

② Making returns a bundle. proven_u8str_create gives a proven_result_u8str_t (that is, {err, value}). Before checking err you do not take value out — that order is the whole of chapter 87.

③ The capacity is “by content”. The 64 of create(alloc, 64) is the number of bytes of content to hold, and the library internally takes one more byte for the NUL. That is how as_cstr can hand out a C string without copying.

④ The failure path gives back too. If formatting fails, the string taken so far is returned with destroy before the error is raised. Grow this pattern and it becomes chapter 87′s goto cleanup idiom.

⑤ The place where ownership passes is explicit. *out = line; is that place. After this line the string’s owner is the caller, and the responsibility to destroy it is the caller’s too.

⑥ Destroying empties the struct. That the length prints as 0 after destroy is the evidence. It is so that the returned buffer is not still pointed at, and the contract that a destroyed object is not used again stands as it is.

/* ① taking value out without checking */
proven_u8str_t s = proven_u8str_create(alloc, 64).value;   /* rubbish on failure */

/* ② destroying with a different allocator */
proven_u8str_destroy(other_alloc, &s);                     /* contract violation */

/* ③ holding a view longer than its original */
proven_u8str_view_t v = proven_u8str_as_view(&s);
proven_u8str_destroy(alloc, &s);
proven_println("{}", PROVEN_ARG(v));                       /* reads a dead place */

/* ④ forgetting PROVEN_ARG */
proven_println("count={}", count);                         /* does not compile */

86.6 Attaching it to your own project — a minimal Makefile

To avoid typing the two lines above every time, use chapter 96′s make. Supposing the library has been put whole into vendor/proven, this much suffices.

CC      = cc
CFLAGS  = -std=c23 -Wall -Wextra -Werror -O2 -Ivendor/proven/include
VSRC    = $(wildcard vendor/proven/src/proven/*.c) \
          $(wildcard vendor/proven/platform/*.c)
VOBJ    = $(VSRC:.c=.o)

app: app.o $(VOBJ)
  $(CC) $^ -lm -o $@

clean:
  rm -f app app.o $(VOBJ)

Only three things need be known. -I tells it where to find <proven.h> (chapter 54). platform/ is the thin layer that calls the operating system, so when going to bare metal only this line is removed (chapter 94). -lm joins the mathematical functions that real-number formatting uses — take reals out of the formatter (chapter 94′s PROVEN_FMT_NO_FLOAT) and this is not needed either.

The first program has run. Yet the proven_println just used can in fact fail too — because the band going to the screen may break (chapter 10). This function returns an error but does not compel a check, and that choice itself is a good entrance to understanding this library’s error model. The next chapter is that.