Frama-C ACSL There were quite a few posts recently that were concerned with ACSL, and a few more are planned for the near future. ACSL is a specification language for C (comparable with JML for Java, for those who know about JML). Some people call it a BISL, for “Behavioral Interface...
Read MoreAn insightful interjection Stephen Canon, whose explanations about the fine points of floating-point I have appreciated on StackOverflow chimed in on the subject of the restrict qualifier. With minor edits for consistency with this blog's formatting: Consider memcpy(); its arguments are declared restrict. This not only means that the source...
Read MoreThe restrict keyword in C99 C99 introduced a restrict keyword. The intention is to let the programmer specify the absence of alias between some inputs of a function ey is writing. Consider the function: int f1(int * restrict p int * restrict q) { *p = 1; *q = 2;...
Read More