1/*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 */
10
11/*
12 * AutoCorres simplification of compound expressions.
13 *
14 * In C, each of the boolean expressions below is simple.
15 * However, C-parser needs to generate a guard for some subexpressions,
16 * and so it turns each expression into a complicated statement.
17 *
18 * One way to simplify them is by rewriting each expression into the form
19 *   guard G; <use expr>
20 * where G contains all the necessary guards for the expr.
21 *
22 * This makes it easier, for example, for the user to separate
23 * the correctness and definedness qualities of the generated code.
24 *
25 * Currently, AutoCorres can do this simplification in some cases,
26 * but cannot simplify any of the expressions below.
27 */
28#define NULL ((void*)0)
29
30void f1(int *p) {
31  if (p != NULL && *p == 0) *p = 1;
32}
33
34struct ure {
35  int n;
36};
37
38void f2(struct ure *p) {
39  if (p != NULL && p->n == 0) p->n = 1;
40}
41
42void fancy(int *p) {
43  if (p != NULL && (p[0] == 0 || p[1] == 0)) {
44    p[0] = p[1];
45  }
46}
47
48void loop(int *p) {
49  while (p != NULL && *p == 0) {
50    p++;
51  }
52}
53
54int arith(int x, int y) {
55  return x / y == 0 || y / x == 0;
56}
57