make sure SPDX license identifiers are in all files

Signed-off-by: Reto Achermann <[email protected]>
verus-lang · Apr 24, 2024 · 5d49600 · 5d49600
1 parent 2166b36
commit 5d49600
Show file tree

Hide file tree

Showing 17 changed files with 45 additions and 0 deletions.
diff --git a/verified-node-replication/src/constants.rs b/verified-node-replication/src/constants.rs
@@ -1,5 +1,6 @@
 // Verified Node Replication Library
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 //! Defines constants that are being used by the library, both in the execution and the
 //! verification. The constants mostly define the size of the log, and certain thresholds
 //! when warnings are being printed etc.

diff --git a/verified-node-replication/src/exec/context.rs b/verified-node-replication/src/exec/context.rs
@@ -1,5 +1,6 @@
 // Verified Node Replication Library
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 #[allow(unused_imports)]
 use builtin::*;
 use builtin_macros::*;

diff --git a/verified-node-replication/src/exec/mod.rs b/verified-node-replication/src/exec/mod.rs
@@ -1,3 +1,6 @@
+// Verified Node Replication Library
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 #[allow(unused_imports)]
 use builtin::*;
 use builtin_macros::*;

diff --git a/verified-node-replication/src/exec/replica.rs b/verified-node-replication/src/exec/replica.rs
@@ -1,3 +1,6 @@
+// Verified Node Replication Library
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 #[allow(unused_imports)]
 use builtin::*;
 use builtin_macros::*;

diff --git a/verified-node-replication/src/exec/rwlock.rs b/verified-node-replication/src/exec/rwlock.rs
@@ -1,3 +1,6 @@
+// Verified Node Replication Library
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 #[allow(unused_imports)]
 use builtin::*;
 use builtin_macros::*;

diff --git a/verified-node-replication/src/exec/utils.rs b/verified-node-replication/src/exec/utils.rs
@@ -1,3 +1,6 @@
+// Verified Node Replication Library
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 #[allow(unused_imports)]
 use builtin::*;
 use builtin_macros::*;

diff --git a/verified-node-replication/src/lib.rs b/verified-node-replication/src/lib.rs
@@ -1,5 +1,8 @@
 // Verified Node Replication Library
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! # Verified Node Replication Library
+//!
 //! This library is a verified version of the [node-replicatin library](https://github.com/vmware/node-replication/)
 //! that allows for the construction of replicated, concurrent data structures.
 //!

diff --git a/verified-node-replication/src/spec/cyclicbuffer.rs b/verified-node-replication/src/spec/cyclicbuffer.rs
@@ -1,5 +1,6 @@
 // Verified Node Replication Library
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 #[allow(unused_imports)]
 use builtin::*;
 use builtin_macros::*;

diff --git a/verified-node-replication/src/spec/flat_combiner.rs b/verified-node-replication/src/spec/flat_combiner.rs
@@ -1,3 +1,6 @@
+// Verified Node Replication Library
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 #[allow(unused_imports)]
 use builtin::*;
 use builtin_macros::*;

diff --git a/verified-node-replication/src/spec/linearization.rs b/verified-node-replication/src/spec/linearization.rs
@@ -1,3 +1,6 @@
+// Verified Node Replication Library
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 // The Linearization Proof
 #[allow(unused_imports)]
 use builtin::*;

diff --git a/verified-node-replication/src/spec/mod.rs b/verified-node-replication/src/spec/mod.rs
@@ -1,3 +1,6 @@
+// Verified Node Replication Library
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 // some types and utilities
 pub mod types;
 pub mod utils;

diff --git a/verified-node-replication/src/spec/rwlock.rs b/verified-node-replication/src/spec/rwlock.rs
@@ -1,3 +1,6 @@
+// Verified Node Replication Library
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 #[allow(unused_imports)]
 use builtin::*;
 use builtin_macros::*;

diff --git a/verified-node-replication/src/spec/simple_log.rs b/verified-node-replication/src/spec/simple_log.rs
@@ -1,3 +1,6 @@
+// Verified Node Replication Library
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 use builtin::*;
 use builtin_macros::*;
 use state_machines_macros::*;

diff --git a/verified-node-replication/src/spec/types.rs b/verified-node-replication/src/spec/types.rs
@@ -1,3 +1,6 @@
+// Verified Node Replication Library
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 #[allow(unused_imports)]
 use builtin::*;
 use builtin_macros::*;

diff --git a/verified-node-replication/src/spec/unbounded_log.rs b/verified-node-replication/src/spec/unbounded_log.rs
@@ -1,3 +1,6 @@
+// Verified Node Replication Library
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 // rust_verify/tests/example.rs ignore
 #[allow(unused_imports)]
 use builtin::*;

diff --git a/verified-node-replication/src/spec/unbounded_log_refines_simplelog.rs b/verified-node-replication/src/spec/unbounded_log_refines_simplelog.rs
@@ -1,3 +1,6 @@
+// Verified Node Replication Library
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 // rust_verify/tests/example.rs ignore
 #[allow(unused_imports)]
 use builtin::*;

diff --git a/verified-node-replication/src/spec/utils.rs b/verified-node-replication/src/spec/utils.rs
@@ -1,3 +1,6 @@
+// Verified Node Replication Library
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
 #[allow(unused_imports)]
 use builtin::*;
 use builtin_macros::*;