Root/b2/relop.c

1/*
2 * relop.c - Relational operators
3 *
4 * Copyright 2012 by Werner Almesberger
5 *
6 * This program is free software; you can redistribute it and/or modify
7 * it under the terms of the GNU General Public License as published by
8 * the Free Software Foundation; either version 2 of the License, or
9 * (at your option) any later version.
10 */
11
12
13#include <stdlib.h>
14#include <stdio.h>
15
16#include "relop.h"
17
18
19/*
20 * Operator to use for
21 *
22 * (A op B) -> forall X: !(X opa A) -> !(X opb B))
23 *
24 * This is for unlimited sets of values. For limited sets of values, we could
25 * decide also in some edge cases, but let's save such sophistication for
26 * later.
27 */
28
29
30static const enum relop unreachable_op[idx_n][idx_n] = {
31#include "unreachable.inc"
32};
33
34
35static int relop2index(enum relop op)
36{
37    switch (op) {
38    case rel_lt:
39        return idx_lt;
40    case rel_le:
41        return idx_le;
42    case rel_eq:
43        return idx_eq;
44    case rel_ge:
45        return idx_ge;
46    case rel_gt:
47        return idx_gt;
48    default:
49        abort();
50    }
51}
52
53
54int relop_unreachable(enum relop opa, enum relop opb,
55    const void *a, const void *b,
56    int (*cmp)(const void *a, enum relop op, const void *b, const void *user),
57    const void *user)
58{
59    return cmp(a,
60        unreachable_op[relop2index(opa)][relop2index(opb)], b, user);
61}
62
63
64void dump_relop(FILE *file, enum relop op)
65{
66    switch (op) {
67    case rel_lt:
68        fprintf(file, "<");
69        break;
70    case rel_le:
71        fprintf(file, "<=");
72        break;
73    case rel_eq:
74        fprintf(file, "=");
75        break;
76    case rel_ge:
77        fprintf(file, ">=");
78        break;
79    case rel_gt:
80        fprintf(file, ">");
81        break;
82    default:
83        abort();
84    }
85}
86

Archive Download this file

Branches:
master



interactive