Merge pull request #460 from verus-lang/new_varlength_ptr_lib

changes to ptr library
verus-lang · Nov 13, 2023 · 6218a43 · 6218a43
2 parents 8aee1d0 + c867130
commit 6218a43
Show file tree

Hide file tree

Showing 34 changed files with 1,767 additions and 221 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -106,4 +106,5 @@ jobs:
           vargo clean
           vargo build
           $env:VERUS_Z3_PATH = "$(Get-Location)/z3"; vargo test -p rust_verify_test --test basic
+          $env:VERUS_Z3_PATH = "$(Get-Location)/z3"; vargo test -p rust_verify_test --test layout
         shell: powershell
diff --git a/dependencies/syn/src/gen/clone.rs b/dependencies/syn/src/gen/clone.rs
diff --git a/dependencies/syn/src/gen/debug.rs b/dependencies/syn/src/gen/debug.rs
diff --git a/dependencies/syn/src/gen/eq.rs b/dependencies/syn/src/gen/eq.rs
diff --git a/dependencies/syn/src/gen/fold.rs b/dependencies/syn/src/gen/fold.rs
diff --git a/dependencies/syn/src/gen/hash.rs b/dependencies/syn/src/gen/hash.rs
diff --git a/dependencies/syn/src/gen/visit.rs b/dependencies/syn/src/gen/visit.rs
diff --git a/dependencies/syn/src/gen/visit_mut.rs b/dependencies/syn/src/gen/visit_mut.rs
diff --git a/dependencies/syn/src/item.rs b/dependencies/syn/src/item.rs
@@ -72,7 +72,7 @@ ast_enum_of_structs! {
 
         /// Tokens forming an item not interpreted by Syn.
         Verbatim(TokenStream),
-        
+
         // Verus
         Global(Global),
 

diff --git a/dependencies/syn/src/lib.rs b/dependencies/syn/src/lib.rs
@@ -458,10 +458,10 @@ mod whitespace;
 mod verus;
 pub use crate::verus::{
     Assert, AssertForall, Assume, BigAnd, BigOr, Closed, DataMode, Decreases, Ensures, ExprHas,
-    ExprIs, FnMode, Invariant, InvariantEnsures, InvariantNameSet, InvariantNameSetAny,
-    InvariantNameSetNone, Mode, ModeExec, ModeGhost, ModeProof, ModeSpec, ModeSpecChecked,
-    ModeTracked, Open, OpenRestricted, Publish, Recommends, Requires, RevealHide,
-    SignatureDecreases, SignatureInvariants, Specification, TypeFnSpec, View, Global,
+    ExprIs, FnMode, Global, GlobalInner, GlobalLayout, GlobalSizeOf, Invariant, InvariantEnsures,
+    InvariantNameSet, InvariantNameSetAny, InvariantNameSetNone, Mode, ModeExec, ModeGhost,
+    ModeProof, ModeSpec, ModeSpecChecked, ModeTracked, Open, OpenRestricted, Publish, Recommends,
+    Requires, RevealHide, SignatureDecreases, SignatureInvariants, Specification, TypeFnSpec, View,
 };
 
 mod gen {

diff --git a/dependencies/syn/src/token.rs b/dependencies/syn/src/token.rs
@@ -737,6 +737,7 @@ define_keywords! {
     "has"         pub struct Has          /// `has`
     "global"      pub struct Global       /// `global`
     "size_of"     pub struct SizeOf       /// `size_of`
+    "layout"      pub struct Layout       /// `layout`
 }
 
 define_punctuation! {
@@ -953,6 +954,7 @@ macro_rules! export_token_macro {
             [has]         => { $crate::token::Has };
             [global]      => { $crate::token::Global };
             [size_of]     => { $crate::token::SizeOf };
+            [layout]      => { $crate::token::Layout };
             [FnSpec]      => { $crate::token::FnSpec };
             [&&&]         => { $crate::token::BigAnd };
             [|||]         => { $crate::token::BigOr };