rerun parser/translator

GaloisInc · Nov 1, 2023 · 3c115d0 · 3c115d0
1 parent 0a11013
commit 3c115d0
Show file tree

Hide file tree

Showing 5 changed files with 45 additions and 0 deletions.
diff --git a/archived/functions-norm-lite.what4.gz b/archived/functions-norm-lite.what4.gz
diff --git a/archived/functions-norm.what4.gz b/archived/functions-norm.what4.gz
diff --git a/archived/instructions-norm-lite.what4.gz b/archived/instructions-norm-lite.what4.gz
diff --git a/archived/instructions-norm.what4.gz b/archived/instructions-norm.what4.gz
diff --git a/data/parsed/extra_defs.sexpr b/data/parsed/extra_defs.sexpr
@@ -661,13 +661,31 @@
               (StmtBlock
                 (list
                   (StmtReturn Nothing)))))))))
+  (DefCallable
+    (QualifiedIdentifier AArch32 CheckITEnabled)
+    (list
+      (SymDecl
+        mask
+        (TypeFun
+          bits
+          (ExprLitNat 4))))
+    Nothing
+    (Just
+      (StmtBlock
+        (list
+          (StmtReturn Nothing)))))
   (DefCallable
     (QualifiedIdentifier Any initGlobals)
     (list)
     Nothing
     (Just
       (StmtBlock
         (list
+          (StmtAssign
+            (LValVarRef
+              (QualifiedIdentifier Any ShouldAdvanceIT))
+            (ExprVarRef
+              (QualifiedIdentifier Any TRUE)))
           (StmtCall
             (QualifiedIdentifier Any setDefaultCond)
             (list))))))
@@ -1273,6 +1291,33 @@
                     (QualifiedIdentifier Any NextInstrAddr)
                     (list)))))
             (list)
+            Nothing)
+          (StmtIf
+            (ExprBinOp
+              "&&"
+              (ExprBinOp
+                "&&"
+                (ExprBinOp
+                  "=="
+                  (ExprVarRef
+                    (QualifiedIdentifier Any __ThisInstrEnc))
+                  (ExprVarRef
+                    (QualifiedIdentifier Any __T16)))
+                (ExprBinOp
+                  "=="
+                  (ExprMember
+                    (ExprVarRef
+                      (QualifiedIdentifier Any PSTATE))
+                    T)
+                  (ExprLitBin '1')))
+              (ExprVarRef
+                (QualifiedIdentifier Any ShouldAdvanceIT)))
+            (StmtBlock
+              (list
+                (StmtCall
+                  (QualifiedIdentifier AArch32 ITAdvance)
+                  (list))))
+            (list)
             Nothing)))))
   (DefCallable
     (QualifiedIdentifier Any ThisInstrAddr)