This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Z3EncodingExample | |
module HS = FStar.HyperStack | |
module B = LowStar.Buffer | |
let hloc_t (inv:HS.mem -> Type0) = fp:(h0:HS.mem { inv h0 } -> GTot B.loc) { | |
forall (h0 h1:HS.mem). {:pattern fp h0; fp h1} // hloc_buffer_nonworking works if we remove this pattern | |
inv h0 /\ | |
(exists l'. B.modifies l' h0 h1 /\ B.loc_disjoint (fp h0) l') ==> inv h1 | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
From fa2732b0fc67cdd1a1b2c67e0ce3c0f1df3f705f Mon Sep 17 00:00:00 2001 | |
From: Landon Fuller <[email protected]> | |
Date: Tue, 1 Sep 2020 10:05:00 -0600 | |
Subject: [PATCH 01/14] emacs-devel: add experimental native_comp variant | |
emacs-devel: add workaround to fix handling of next-read-file-uses-dialog-p when using +native_comp | |
--- | |
editors/emacs/Portfile | 20 +++++++++++++++++++ | |
.../files/patch-Makefile.in-native_comp.diff | 12 +++++++++++ | |
...ive-comp-next-read-file-uses-dialog-p.diff | 13 ++++++++++++ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
entry: mips_init() | |
Cache info: | |
picache_stride = 4096 | |
picache_loopcount = 8 | |
pdcache_stride = 4096 | |
pdcache_loopcount = 8 | |
max line size = 32 | |
cpu0: MIPS Technologies processor v73.151 | |
MMU: Standard TLB, 64 entries (4K 16K 64K 256K 1M 16M 64M 256M pg sizes) | |
L1 i-cache: 4 ways of 256 sets, 32 bytes per line |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
diff --git a/sys/dev/bwn/bwn_mac.c b/sys/dev/bwn/bwn_mac.c | |
deleted file mode 100644 | |
index 42452c356b0..00000000000 | |
--- a/sys/dev/bwn/bwn_mac.c | |
+++ /dev/null | |
@@ -1,174 +0,0 @@ | |
-/*- | |
- * Copyright (c) 2015 Landon Fuller <[email protected]> | |
- * All rights reserved. | |
- * |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
bwn_v4_ucode_load="YES" | |
bwn_v4_lp_ucode_load="YES" | |
if_bwn_load="YES" | |
if_bwn_pci_load="YES" | |
hw.bwn_pci.preferred="1" | |
hw.bwn_pci.attach_untested="1" |
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/** | |
* A unique PIC-specific interrupt source. | |
*/ | |
struct intr_irqsrc { | |
device_t isrc_dev; /**< PIC that registered this isrc */ | |
u_int isrc_irq; /**< globally unique abstract IRQ number */ | |
u_int isrc_flags; /**< interrupt flags. see INTR_ISRCF_* */ | |
char isrc_name[INTR_ISRC_NAMELEN]; /**< interrupt name (assigned in intr_isrc_register()) */ | |
cpuset_t isrc_cpu; /**< on which CPUs is enabled */ | |
u_int isrc_index; /**< base index into the global intrcnt array; isrc_count |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/* | |
* Declared at: | |
* include/linux/bcm47xx_nvram.h:39 | |
* | |
* Called by: | |
* brcmf_fw_request_nvram_done() | |
* | |
* Referenced by: | |
* drivers/net/wireless/broadcom/brcm80211/brcmfmac/firmware.c:464 | |
*/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
landonf:srcport> ./obj/srcport --src-path="${FREEBSD_SRC}" --host-path="${FREEBSD_SRC}/sys/dev/siba" \ | |
${FREEBSD_SRC}/sys/dev/bwn/*.c -- \ | |
-I${FREEBSD_SRC}/sys -I${FREEBSD_SRC}/sys/sys -I${FREEBSD_OBJ} \ | |
-I${FREEBSD_OBJ}/../modules/bwn_pci \ | |
-D_KERNEL -nostdinc -fno-builtin \ | |
-Wno-pointer-sign -Wno-format | |
Scanning /home/landonf/Documents/Code/FreeBSD/freebsd/sys/dev/bwn/bwn_mac.c | |
Scanning /home/landonf/Documents/Code/FreeBSD/freebsd/sys/dev/bwn/if_bwn.c | |
Scanning /home/landonf/Documents/Code/FreeBSD/freebsd/sys/dev/bwn/if_bwn_pci.c |
NewerOlder