aboutsummaryrefslogtreecommitdiffstatshomepage
diff options
-rw-r--r--validation/linear/logical-phi0.c49
1 files changed, 49 insertions, 0 deletions
diff --git a/validation/linear/logical-phi0.c b/validation/linear/logical-phi0.c
new file mode 100644
index 00000000..92ba3bc5
--- /dev/null
+++ b/validation/linear/logical-phi0.c
@@ -0,0 +1,49 @@
+int a(void);
+int b(void);
+int c(void);
+
+static int laa(void)
+{
+ return (a() && b()) && c();
+}
+
+static int lao(void)
+{
+ return (a() && b()) || c();
+}
+
+static int loa(void)
+{
+ return (a() || b()) && c();
+}
+
+static int loo(void)
+{
+ return (a() || b()) || c();
+}
+
+static int raa(void)
+{
+ return a() && (b() && c());
+}
+
+static int rao(void)
+{
+ return a() && (b() || c());
+}
+
+static int roa(void)
+{
+ return a() || (b() && c());
+}
+
+static int roo(void)
+{
+ return a() || (b() || c());
+}
+
+/*
+ * check-name: bad-logical-phi0
+ * check-command: sparse -vir -flinearize=last $file
+ * check-known-to-fail
+ */