Skip to content

Instantly share code, notes, and snippets.

🌴
On vacation

Kiwamu Okabe master-q

🌴
On vacation
Block or report user

Report or block master-q

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@master-q
master-q / 00run.sh
Created May 27, 2019
How to inject ATS's DWARF debug info
View 00run.sh
$ gcc -g -I /home/kiwamu/src/ATS-Postiats/ccomp/runtime/ -I /home/kiwamu/src/ATS-Postiats/ main_dats.c
$ gdb a.out
(gdb) b main.dats:atspre_g0int_add_int
Breakpoint 1 at 0x120a: file /home/kiwamu/src/ATS-Postiats/prelude/CATS/integer.cats, line 157.
(gdb) run
Starting program: /home/kiwamu/src/idiomaticca/regress/noinc/arithmetic_op/a.out
Breakpoint 1, atspre_g0int_add_int (x1=1, x2=2) at /home/kiwamu/src/ATS-Postiats/prelude/CATS/integer.cats:157
157 (atstype_int x1, atstype_int x2) { return (x1 + x2) ; }
(gdb) bt
@master-q
master-q / memo.rd
Created May 27, 2019
#Vala はどうやって #DWARF を吐くのか
View memo.rd
= ValaはどうやってDWARFを吐くのか
[2019-05-27 16:20]
<<<Vala
<<<DWARF
== 参考
"Projects/Genie/Developing - GNOME Wiki!" https://wiki.gnome.org/Projects/Genie/Developing
"Valaのデバッグ[メモ] | TIPS" http://1204lts.blogspot.com/2014/01/vala.html
@master-q
master-q / cat.c
Last active Feb 1, 2019
corrodeにBSDなcatをかけてみた
View cat.c
/* $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 / cat.c
Last active Feb 1, 2019
C2RustにBSDなcatをかけてみた
View cat.c
/* $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.
*
View vcc-survey.rd
= VCCサーベイ
[2018-04-15 15:00]
<<<VCC
<<<サーベイ
https://archive.codeplex.com/?p=vcc
論文を以下に置いた:
@master-q
master-q / memo.rd
Created Nov 12, 2018
VeriFastでFreeRTOSに注釈を付ける
View memo.rd
= VeriFastFreeRTOSに注釈を付ける
[2018-06-01 09:59]
<<<VeriFast
<<<FreeRTOS
<<<C99
eldeshさんのアドバイスに従ってもっとも小さい実例からはじめよう。
https://github.com/metasepi/amazon-freertos
View prolog-intro-report.md

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 Oct 12, 2018
Try to verify FreeRTOS using VeriFast
View Try_to_verify_FreeRTOS_using_VeriFast.rd
= VeriFastFreeRTOSに注釈を付ける
[2018-06-01 09:59]
<<<VeriFast
<<<FreeRTOS
<<<C99
eldeshさんのアドバイスに従ってもっとも小さい実例からはじめよう。
== lib/FreeRTOS/tasks.c
@master-q
master-q / ATS_News_October_2018.rd
Last active Oct 12, 2018
Latest news on ATS language - October 2018
View ATS_News_October_2018.rd
= ATS最新動向 2018-10-10
[2018-10-10 15:08]
<<<ATS
<<<最新動向
<<<サーベイ
=== 最新のまとめ
http://b.hatena.ne.jp/masterq/ats
View gist:e987ef488fdefa2c597e74df88a6cf18
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
You can’t perform that action at this time.