Open-Source Projects

03/22/2019

05:22 PM C Instrumentation Framework Bug #9559 (Closed): C back-end incorrectly prints wide character strings

Implemented in commit:936ef2a.

05:22 PM C Instrumentation Framework Revision 936ef2a3: Update Aspectator and add test cases

05:20 PM Aspectator Revision 0736cbe7: Add support for printing wide character strings

Besides, improve printing of normal strings. Before non-ASCII ones were
represented with \ooo. Now they are represent...

03/21/2019

02:12 PM C Instrumentation Framework Feature #9561 (Closed): C back-end should support __floatn type specifiers

I supported different floatn types in commit:739b54d to master.

02:11 PM C Instrumentation Framework Revision 739b54dd: Update Apectator and add test case

02:10 PM Aspectator Revision 87c72faf: Support floatn types

Implements https://forge.ispras.ru/issues/9561.

01:42 PM Aspectator Revision 6ee6d55d: Print one error message for unsupported type specifiers rather 3 ones

12:26 PM C Instrumentation Framework Feature #9561 (Closed): C back-end should support __floatn type specifiers

GCC does that already: https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html.

11:37 AM Deductive Verification Tools for Linux Kernel Bug #9560: Frama-C (CIL) does not support initialization of wide character arrays with wide character literals like GCC

I revealed that Frama-C (CIL) likes just defined _wchar_t_ and something like:...

11:29 AM Deductive Verification Tools for Linux Kernel Bug #9560 (New): Frama-C (CIL) does not support initialization of wide character arrays with wide character literals like GCC

For the attached file GCC 7 provides no warnings and errors with the following command (Linux x86_64):...