From 6281499ca2e3b277740fe57556bce3cb9d524a93 Mon Sep 17 00:00:00 2001
From: Ali Kheradmand <a.i.kheradmand@gmail.com>
Date: Wed, 4 Apr 2018 01:54:33 -0400
Subject: [PATCH] test for https://github.com/kframework/k-legacy/issues/2407

---
 tranlation-validation/simple/c.k          | 10 ++++++++
 tranlation-validation/simple/empty        |  1 +
 tranlation-validation/simple/test-spec.k  | 10 ++++++++
 tranlation-validation/simple/test.k       | 30 +++++++++++++++++++++++
 tranlation-validation/simple/test2-spec.k | 15 ++++++++++++
 5 files changed, 66 insertions(+)
 create mode 100644 tranlation-validation/simple/c.k
 create mode 100644 tranlation-validation/simple/empty
 create mode 100644 tranlation-validation/simple/test-spec.k
 create mode 100644 tranlation-validation/simple/test.k
 create mode 100644 tranlation-validation/simple/test2-spec.k

diff --git a/tranlation-validation/simple/c.k b/tranlation-validation/simple/c.k
new file mode 100644
index 0000000..d56f524
--- /dev/null
+++ b/tranlation-validation/simple/c.k
@@ -0,0 +1,10 @@
+module C
+
+    //=========
+    syntax Bool ::= vars(List)
+    //========
+
+
+
+
+endmodule
\ No newline at end of file
diff --git a/tranlation-validation/simple/empty b/tranlation-validation/simple/empty
new file mode 100644
index 0000000..2c3f05b
--- /dev/null
+++ b/tranlation-validation/simple/empty
@@ -0,0 +1 @@
+@val(12,12,false)
\ No newline at end of file
diff --git a/tranlation-validation/simple/test-spec.k b/tranlation-validation/simple/test-spec.k
new file mode 100644
index 0000000..45716ba
--- /dev/null
+++ b/tranlation-validation/simple/test-spec.k
@@ -0,0 +1,10 @@
+
+module SPEC
+  imports TEST
+
+  rule <k> V:Val => I:Int </k>
+  //requires #noUndef(V)
+
+  //rule <k> V:NUVal => I:Int </k>
+
+endmodule
diff --git a/tranlation-validation/simple/test.k b/tranlation-validation/simple/test.k
new file mode 100644
index 0000000..b0f71b6
--- /dev/null
+++ b/tranlation-validation/simple/test.k
@@ -0,0 +1,30 @@
+//require "c.k"
+
+module TEST
+    //imports C
+
+    syntax Val ::= "@undef" [smtlib(val_undef)]
+    syntax Val ::= "@val" "("Int","Int","Bool")" [smtlib(smt_val)] //int,width,signed
+
+    //syntax Val ::= NUVal
+    //syntax NUVal ::=  "@val" "("Int","Int","Bool")"
+
+
+    //=========
+    //syntax Bool ::= vars(List)
+    //========
+
+
+    configuration
+    <T>
+        <k> $PGM:Val </k>
+    </T>
+
+
+    rule <k> @val(I:Int,_,_) => I </k>
+
+
+    syntax Bool ::= "#noUndef" "(" Val ")" [function]//[function, smtlib(no_undef)]
+    rule #noUndef(@val(_,_,_)) => true //[smt-lemma]
+    rule #noUndef(@undef) => false     //[smt-lemma]
+endmodule
\ No newline at end of file
diff --git a/tranlation-validation/simple/test2-spec.k b/tranlation-validation/simple/test2-spec.k
new file mode 100644
index 0000000..a7349c7
--- /dev/null
+++ b/tranlation-validation/simple/test2-spec.k
@@ -0,0 +1,15 @@
+
+module SPEC
+  imports TEST
+
+
+  rule <k> V:Val </k>
+  //requires #noUndef(V)
+  ensures vars(ListItem(V) ListItem(0))
+
+
+  rule <k> I:Int </k>
+  ensures vars(ListItem(I) ListItem(0))
+  [trusted]
+
+endmodule