NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library C_pp_examples

Require Import ssreflect ssrbool.
Require Import ZArith_ext.
Require Import machine_int.
Import MachineInt.
Require Import C_pp C_examples.

Goal (typ_to_string example_m.pair_ab "" = "struct pair { unsigned int a; unsigned int b; }")%string.

Goal (typ_value_to_string example_m.pair_ab example_m.pair_ab_14 "" = "{ 1, 4 }")%string.

Goal (pp_exp example_m.var_expr "" = "apair")%string.

Goal (pp_cmd example_m.test_prog "" = "x = 0; x = *((y) + (1)); z = malloc(1); *(z) = y; free(y); free(z);")%string.

Goal (typ_to_string inplace_reverse_list_m.C_lst "" = "struct C_lst { unsigned int data; struct C_lst * next; }")%string.

Goal (pp_exp inplace_reverse_list_m.NULL "" = "(struct C_lst *)(0)")%string.

Goal (pp_cmd inplace_reverse_list_m.reverse_list "" = "ret = (struct C_lst *)(0); while (!((_Bool)((i) == ((struct C_lst *)(0))))) { rem = *(&(i->next)); *(&(i->next)) = ret; ret = i; i = rem; }")%string.