master-q

$ 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

= 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

/*	$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

/*	$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

= VCCサーベイ
[2018-04-15 15:00]

<<<VCC
<<<サーベイ

https://archive.codeplex.com/?p=vcc

論文を以下に置いた:

master-q

= VeriFastでFreeRTOSに注釈を付ける
[2018-06-01 09:59]

<<<VeriFast
<<<FreeRTOS
<<<C99

eldeshさんのアドバイスに従ってもっとも小さい実例からはじめよう。

https://github.com/metasepi/amazon-freertos

master-q

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

= VeriFastでFreeRTOSに注釈を付ける
[2018-06-01 09:59]

<<<VeriFast
<<<FreeRTOS
<<<C99

eldeshさんのアドバイスに従ってもっとも小さい実例からはじめよう。

== lib/FreeRTOS/tasks.c

master-q

= ATS最新動向 2018-10-10
[2018-10-10 15:08]

<<<ATS
<<<最新動向
<<<サーベイ

=== 最新のまとめ

http://b.hatena.ne.jp/masterq/ats

master-q

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