Merge pull request #881 from herd/fix-tests

[herd] Fix a few glitches in tests
herd · Dec 3, 2024 · f14f8ef · f14f8ef
2 parents cd9b4a5 + 61e3127
commit f14f8ef
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 4 deletions.
diff --git a/herd/tests/instructions/AArch64.self/NORUN b/herd/tests/instructions/AArch64.self/NORUN
@@ -13,3 +13,5 @@ S15
 S16
 S17
 S23
+#This test faults on non-existing instruction
+S20
diff --git a/herd/tests/instructions/AArch64/A236.litmus b/herd/tests/instructions/AArch64/A236.litmus
@@ -1,4 +1,4 @@
-AArch64 236
+AArch64 A236
 
 (* Tests MVN Register instruction *)
 (* Remember inverting 00 -> 11 which is 0 to -1 in 2s complement *)

diff --git a/herd/tests/instructions/AArch64/A236.litmus.expected b/herd/tests/instructions/AArch64/A236.litmus.expected
@@ -1,10 +1,10 @@
-Test 236 Required
+Test A236 Required
 States 1
 0:X0=-1; 0:X3=-2;
 Ok
 Witnesses
 Positive: 1 Negative: 0
 Condition forall (0:X0=-1 /\ 0:X3=-2)
-Observation 236 Always 1 0
+Observation A236 Always 1 0
 Hash=8205eb706c7f2a58368a8bdc3b855c37
 
diff --git a/herd/tests/instructions/AArch64/L086.litmus b/herd/tests/instructions/AArch64/L086.litmus
@@ -1,4 +1,6 @@
 AArch64 L086
+(* Allocate register X1 to X1 *)
+Stable=X1
 {
 0:X0=instr:"ADR X1,.+0";
 }
@@ -8,4 +10,4 @@ L0:           ;
   LDR W2,[X1] ;
   CMP W0,W2   ;
   CSET W3,EQ  ;
-forall 0:X3=1  
+forall 0:X3=1
-Original file line number
+Diff line change
@@ Expand Up / @@ -13,3 +13,5 @@ S15 @@
     S16
     S17
     S23
+    #This test faults on non-existing instruction
+    S20