test for kframework/k-legacy#2407

tranlation-validation/simple/c.k

@@ -0,0 +1,10 @@
+module C
+
+    //=========
+    syntax Bool ::= vars(List)
+    //========
+
+
+
+
+endmodule

tranlation-validation/simple/empty

@@ -0,0 +1 @@
+@val(12,12,false)

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

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

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