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