Skip to content

Instantly share code, notes, and snippets.

View master-q's full-sized avatar
🌴
On vacation

Kiwamu Okabe master-q

🌴
On vacation
89 followers · 132 following
View GitHub Profile
@master-q
master-q / cat.c
Last active February 1, 2019 08:32
C2RustにBSDなcatをかけてみた
/* $OpenBSD: cat.c,v 1.26 2016/10/19 18:20:25 schwarze Exp $ */
/* $NetBSD: cat.c,v 1.11 1995/09/07 06:12:54 jtc Exp $ */
/*
* Copyright (c) 1989, 1993
* The Regents of the University of California. All rights reserved.
*
* This code is derived from software contributed to Berkeley by
* Kevin Fall.
*
@master-q
master-q / vcc-survey.rd
Created November 27, 2018 00:47
VCCサーベイ
= VCCサーベイ
[2018-04-15 15:00]
<<<VCC
<<<サーベイ
https://archive.codeplex.com/?p=vcc
論文を以下に置いた:
@master-q
master-q / memo.rd
Created November 12, 2018 04:05
VeriFastでFreeRTOSに注釈を付ける
= VeriFastでFreeRTOSに注釈を付ける
[2018-06-01 09:59]
<<<VeriFast
<<<FreeRTOS
<<<C99
eldeshさんのアドバイスに従ってもっとも小さい実例からはじめよう。
https://github.com/metasepi/amazon-freertos
@master-q
master-q / prolog-intro-report.md
Created October 17, 2018 06:30
Prolog入門の感想

Introduction to Prolog (in Japanese) を一通り読んだ感想:

  • 便利だなぁ "変数を含んだ質問では，複数の答えが存在する場合がある． たとえば， saburo の子供は naoyuki と shinji の 2 人がいるから ?- father(saburo, C). の答えは 2 種類存在するはずである． Prolog ではこのような場合，プログラム中での記述の順序にしたがって 答えが表示される．"
  • えーと。これは定義の順に辿って最初に見つかった1つの例が選択されるってことなんです？ "質問 ?- father(G, F), father(F, hyogo). の場合も左から順に処理される． まず father(G, F) の最初の答え G=naoyuki, F=hyogo が求められる．"
  • これでも、、、バックトラックを手作業で制御するとなると、、、記述量が増えませんか？
  • あーspyは便利ですね。
  • でも、、、それってシンボリック実行の方がより強力だと感じます
  • うーん、これCollatzを実装したとしても任意の自然数で停止する証左にならないのでは。。。
  • これ結局実行しているから、バックトラックで枝切りした範囲でしか健全性が主張できないのでは
@master-q
master-q / Try_to_verify_FreeRTOS_using_VeriFast.rd
Created October 12, 2018 01:51
Try to verify FreeRTOS using VeriFast
= VeriFastでFreeRTOSに注釈を付ける
[2018-06-01 09:59]
<<<VeriFast
<<<FreeRTOS
<<<C99
eldeshさんのアドバイスに従ってもっとも小さい実例からはじめよう。
== lib/FreeRTOS/tasks.c
@master-q
master-q / ATS_News_October_2018.rd
Last active October 12, 2018 01:19
Latest news on ATS language - October 2018
= ATS最新動向 2018-10-10
[2018-10-10 15:08]
<<<ATS
<<<最新動向
<<<サーベイ
=== 最新のまとめ
http://b.hatena.ne.jp/masterq/ats
@master-q
master-q / gist:e987ef488fdefa2c597e74df88a6cf18
Created May 7, 2018 08:44
vivado_bitstream_error.log
INFO: [Project 1-604] Checkpoint was created with Vivado v2018.1 (64-bit) build 2188600
open_checkpoint: Time (s): cpu = 00:00:24 ; elapsed = 00:00:50 . Memory (MB): peak = 1945.238 ; gain = 766.211 ; free physical = 1385 ; free virtual = 2781
Command: write_bitstream -force tutorial_bd_wrapper.bit
Attempting to get a license for feature 'Implementation' and/or device 'xc7z020'
INFO: [Common 17-349] Got license for feature 'Implementation' and/or device 'xc7z020'
Running DRC as a precondition to command write_bitstream
INFO: [IP_Flow 19-234] Refreshing IP repositories
INFO: [IP_Flow 19-1704] No user IP repositories specified
INFO: [IP_Flow 19-2313] Loaded Vivado IP repository '/opt/Xilinx/Vivado/2018.1/data/ip'.
INFO: [DRC 23-27] Running DRC with 4 threads
@master-q
master-q / keybase.md
Created January 28, 2018 22:03
keybase.md

Keybase proof

I hereby claim:

  • I am master-q on github.
  • I am masterq (https://keybase.io/masterq) on keybase.
  • I have a public key whose fingerprint is DF60 3D3A 3C15 1B2C DF19 52F4 18DD 4D72 F2CB CA06

To claim this, I am signing this object:

@master-q
master-q / memo.txt
Created January 26, 2018 23:10
WICED StudioにwolfSSLを移植する
= WICED StudioにwolfSSLを移植する
[2017-12-08 15:09]
<<<WICED
<<<Cypress
<<<wolfSSL
https://github.com/wolfSSL/wolfssl/issues/1266 で議論を継続。
== Plan
@master-q
master-q / CPU1_cycle.v
Created December 30, 2017 10:42
Output of CLaSH CPU
// Automatically generated Verilog-2001
module CPU1_cycle(ds,result);
input [4546:0] ds;
output [4546:0] result;
wire [4546:0] case_alt;
wire [4546:0] result_0;
wire [450:0] ds1;
wire [4546:0] case_alt_0;
wire [4546:0] case_alt_1;
wire [4546:0] case_alt_2;