Ufyukyu

up vote 1 down vote favorite This function mocks a function that returns a continuously rising value until overflow occurs. It is like the millis() function in Arduino. To prove the implementation, I need to increment (thus, assign) static variables to keep state between invocations. However, a function that calls mock_millis() should still be able to assign nothing . Is there a way to make WP ignore the assigns clause? static int64_t microseconds = 0; /*@ assigns milliseconds; behavior normal: assumes milliseconds < INT64_MAX; ensures result == old(milliseconds) + 1; ensures milliseconds == old(milliseconds) + 1; behavior overflow: assumes milliseconds == INT64_MAX; ensures result == 0; ensures milliseconds == 0; complete behaviors normal, overflow; disjoi...

千年紀: 2千年紀 世紀: 12世紀 - 13世紀 - 14世紀 十年紀: 1190年代 1200年代 1210年代 1220年代 1230年代 年: 1210年 1211年 1212年 1213年 1214年 1215年 1216年 1213年 （1213 ねん）は、西暦（ユリウス暦）による、平年。 目次 1 他の紀年法 2 カレンダー 3 できごと 4 誕生 5 死去 6 脚注 7 関連項目 他の紀年法 この節は、 ウィキプロジェクト 紀年法 の ガイドライン に基づいて記述されています。この節に大きな変更を加える場合には、あらかじめ上記プロジェクトのノートで提案し、合意を形成してください。 凡例 分類にある「日本」「中国」「中国周辺」「朝鮮」「ベトナム」は地域概念であり、特定の国家をさすものではなく、またその外延は便宜的に定めたものである。特に「*」の付された王朝の分類は仮配置であり、現在も「ガイドライン」のノートで対応を検討中である。 「中国周辺」は、「広義の北アジア、中央アジア、及びこれに隣接する中国の一部地域（ほぼ中央ユーラシアに相当）」を指す。 一段右寄せの箇条に掲げた元号は、その上段の元号を建てた王朝に対抗する私年号である。 仏滅紀元及びユダヤ暦は、現在のところ元年と対応する西暦年から逆算した数を表示しており、旧暦等の暦日の記述とともに確実な出典を確認していないので利用には注意されたい。 皇紀は日本で1873年の太陽暦採用と同時に施行された。 檀紀は大韓民国で1948年から1961年まで公式に使用された。 主体暦は朝鮮民主主義人民共和国で1997年から公式に使用されている。 仏滅紀元は紀元前543年を元年とするタイ仏暦を基準にしている。スリランカなどでは紀元前544年を元年としているので1を加算されたい。 干支 : 癸酉 日本 建暦3年 皇紀1873年 中国 南宋 : 嘉定6年 金 : 崇慶2年、至寧元年旧5月 - 9月14日、貞祐元年9月15日 - 東遼 : 元統元年旧3月 - 中国周辺 西夏 *  : 光...