Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Removing unused modules #539

Merged
merged 2 commits into from
Feb 18, 2025
Merged

Removing unused modules #539

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7c3485b
Run `$FSTAR/.scripts/remove_all_unused_opens.sh krmllib/`
mtzguido Feb 17, 2025
bafc55f
Run `$FSTAR/.scripts/remove_all_unused_opens.sh test/`
mtzguido Feb 17, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 0 additions & 3 deletions krmllib/C.String.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,7 @@
module C.String

module U8 = FStar.UInt8
module U32 = FStar.UInt32

module B = LowStar.Buffer
module M = LowStar.Modifies

open FStar.HyperStack.ST

Expand Down
1 change: 0 additions & 1 deletion krmllib/C.String.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
module C.String

module U8 = FStar.UInt8
module U32 = FStar.UInt32

module B = LowStar.Buffer
Expand Down
1 change: 0 additions & 1 deletion krmllib/C.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@ module C

open FStar.HyperStack.ST

module HS = FStar.HyperStack
module U8 = FStar.UInt8

// This module contains a series of bindings that already exist in C. It receives
Expand Down
2 changes: 0 additions & 2 deletions krmllib/LowStar.Lib.AssocList.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,6 @@ module LowStar.Lib.AssocList
module B = LowStar.Buffer
module HS = FStar.HyperStack
module G = FStar.Ghost
module L = FStar.List.Tot
module U32 = FStar.UInt32
module ST = FStar.HyperStack.ST

module M = FStar.Map
Expand Down
5 changes: 0 additions & 5 deletions krmllib/LowStar.Lib.AssocList.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,14 +4,9 @@ module LowStar.Lib.AssocList

module B = LowStar.Buffer
module HS = FStar.HyperStack
module G = FStar.Ghost
module L = FStar.List.Tot
module U32 = FStar.UInt32
module ST = FStar.HyperStack.ST

module M = FStar.Map
module LL2 = LowStar.Lib.LinkedList2
module LL1 = LowStar.Lib.LinkedList

open FStar.HyperStack.ST
open LowStar.BufferOps
Expand Down
2 changes: 0 additions & 2 deletions krmllib/LowStar.Lib.LinkedList2.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,6 @@ open LowStar.BufferOps
module B = LowStar.Buffer
module HS = FStar.HyperStack
module G = FStar.Ghost
module L = FStar.List.Tot
module U32 = FStar.UInt32
module ST = FStar.HyperStack.ST

module LL1 = LowStar.Lib.LinkedList
Expand Down
1 change: 0 additions & 1 deletion krmllib/TestLib.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ module TestLib
open FStar.HyperStack.ST
open LowStar.Buffer

module HS = FStar.HyperStack
module Buffer = LowStar.Buffer

(** Some test routines *)
Expand Down
1 change: 0 additions & 1 deletion krmllib/compat/C.Compat.String.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
module C.Compat.String

module U8 = FStar.UInt8
module U32 = FStar.UInt32

module B = LowStar.Buffer
Expand Down
1 change: 0 additions & 1 deletion krmllib/compat/C.Compat.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@ module C.Compat

open FStar.HyperStack.ST

module HS = FStar.HyperStack
module U8 = FStar.UInt8

// This module contains a series of bindings that already exist in C. It receives
Expand Down
3 changes: 0 additions & 3 deletions krmllib/compat/C.Nullity.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,9 +37,6 @@ let (!*) (#a: Type) (p: pointer a):
(ensures (fun h0 x h1 -> B.live h1 p /\ x == B.get h0 p 0 /\ h1 == h0)) =
B.index p 0ul

module U32 = FStar.UInt32
module Seq = FStar.Seq
module Heap = FStar.Heap

(* Two pointers with different reads are disjoint *)

Expand Down
2 changes: 0 additions & 2 deletions test/Ctypes2.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,6 @@ open FStar.Mul
open FStar.UInt
open FStar.HyperStack.ST

module M = LowStar.Modifies
module U16 = FStar.UInt16
module U32 = FStar.UInt32

open Ctypes1
Expand Down
1 change: 0 additions & 1 deletion test/Ctypes4.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@ open FStar.UInt
open FStar.HyperStack.ST

module B = LowStar.Buffer
module M = LowStar.Modifies
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U128 = FStar.UInt128
Expand Down
1 change: 0 additions & 1 deletion test/DataTypesEq.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
module DataTypesEq

module SoBuggy = FStar.HyperStack.ST

type t =
| A: UInt32.t -> t
Expand Down
1 change: 0 additions & 1 deletion test/HigherOrder2.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
module HigherOrder2

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module I32 = FStar.Int32
module M = LowStar.Modifies
Expand Down
1 change: 0 additions & 1 deletion test/HigherOrder4.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ module B = LowStar.Buffer
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module M = LowStar.Modifies
module U32 = FStar.UInt32
module I32 = FStar.Int32

open LowStar.BufferOps
Expand Down
1 change: 0 additions & 1 deletion test/Layered.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
module Layered

open FStar.HyperStack.ST
module U32 = FStar.UInt32
module HS = FStar.HyperStack

inline_for_extraction
Expand Down
1 change: 0 additions & 1 deletion test/LinkedList1.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
module LinkedList1

module B = FStar.Buffer
module HS = FStar.HyperStack
module G = FStar.Ghost
module L = FStar.List.Tot
Expand Down
1 change: 0 additions & 1 deletion test/LinkedList2.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ module B = FStar.Buffer
module CN = C.Nullity
module HS = FStar.HyperStack
module G = FStar.Ghost
module L = FStar.List.Tot
module U32 = FStar.UInt32
module MO = FStar.Modifies

Expand Down
1 change: 0 additions & 1 deletion test/LinkedList3.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ open LowStar.BufferOps
module B = LowStar.Buffer
module HS = FStar.HyperStack
module G = FStar.Ghost
module L = FStar.List.Tot
module U32 = FStar.UInt32
module MO = LowStar.Modifies

Expand Down
1 change: 0 additions & 1 deletion test/Lowlevel.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ open FStar.UInt
open FStar.HyperStack.ST

module B = LowStar.Buffer
module M = LowStar.Modifies
module U16 = FStar.UInt16
module U32 = FStar.UInt32

Expand Down
1 change: 0 additions & 1 deletion test/MutualStruct.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@ open FStar.HyperStack.ST

module U64 = FStar.UInt64
module U8 = FStar.UInt8
module SZ = FStar.SizeT

let main () = C.EXIT_SUCCESS // dummy

Expand Down
1 change: 0 additions & 1 deletion test/NoShadow.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@ module NoShadow

module U32 = FStar.UInt32
module U64 = FStar.UInt64
module HS = FStar.HyperStack

open FStar.HyperStack.ST

Expand Down
1 change: 0 additions & 1 deletion test/Rust6.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ open FStar.HyperStack.ST

module B = LowStar.Buffer
module C = LowStar.ConstBuffer
module HS = FStar.HyperStack


inline_for_extraction noextract
Expand Down
1 change: 0 additions & 1 deletion test/Scope.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@ open FStar.Int32
open FStar.HyperStack.ST
open TestLib

module B = FStar.Buffer

let foo (): Stack bool (fun _ -> true) (fun h0 _ h1 -> h0 == h1) =
true
Expand Down
2 changes: 0 additions & 2 deletions test/TotalLoops.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,6 @@ module TotalLoops
open FStar
open FStar.Buffer
open FStar.HyperStack.ST
module UInt32 = FStar.UInt32
module UInt64 = FStar.UInt64

let rec fib
(x: nat)
Expand Down
1 change: 0 additions & 1 deletion test/Underspec.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
module Underspec

open FStar.HyperStack.ST
module U32 = FStar.UInt32

(* Checking that the *_underspec operators actually extract and run
properly. *)
Expand Down
1 change: 0 additions & 1 deletion test/hello-system/SystemNative.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ module SystemNative
module S = FStar.Seq
module B = FStar.Buffer
module U8 = FStar.UInt8
module I32 = FStar.UInt8
module U32 = FStar.UInt32

(* Strings *******************************************************************)
Expand Down
1 change: 0 additions & 1 deletion test/sepcomp/b/B.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
module B
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module Cast = FStar.Int.Cast
module A = A.Top
Expand Down
1 change: 0 additions & 1 deletion test/sepcomp/b/D.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
module D
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module Cast = FStar.Int.Cast
module A = A.Top
Expand Down