From ba480b607c314b672ccf525e05392989a19865c8 Mon Sep 17 00:00:00 2001 From: Jay <83922342+Jayfromthe13th@users.noreply.github.com> Date: Thu, 2 Jan 2025 17:37:23 -0600 Subject: [PATCH] Delete framework/libra-framework/backup_specs/demo.spec.move --- .../backup_specs/demo.spec.move | 23 ------------------- 1 file changed, 23 deletions(-) delete mode 100644 framework/libra-framework/backup_specs/demo.spec.move diff --git a/framework/libra-framework/backup_specs/demo.spec.move b/framework/libra-framework/backup_specs/demo.spec.move deleted file mode 100644 index 4d426607c..000000000 --- a/framework/libra-framework/backup_specs/demo.spec.move +++ /dev/null @@ -1,23 +0,0 @@ -spec ol_framework::demo { - spec module { - pragma verify = true; - } - - spec print_this(account: &signer) { - // should not abort - pragma aborts_if_is_strict; - } - - // TODO in strict mode - spec set_message(account: &signer, message: string::String) { - // pragma aborts_if_is_strict; - // let events = borrow_global(signer::address_of(account)).message_change_events; - // aborts_if event::counter(events) > MAX_U64; - } - - spec get_message(addr: address): string::String { - pragma aborts_if_is_strict; - aborts_if !exists(addr); - - } -}