2021-01-17 22:51 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001576Frama-CKernelpublic2013-11-28 13:47
Assigned Tovirgile 
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in Version 
Summary0001576: declaration of variable of type void accepted
DescriptionRunning "frama-c -wp void.c" on the attached program doesn't report any error message, although declaring i to have type void doesn't make sense.

Vice versa, when "i" is deleted, or when "void i" is deleted, the kernel complains about a syntax error. Therefore, the only possibility to implement a logical constant is to declare "void i" as its parameter.
TagsNo tags attached.
Attached Files
  • c file icon void.c (40 bytes) 2013-11-28 13:42 -
    //@ logic integer myZero(void i) = 0;
    c file icon void.c (40 bytes) 2013-11-28 13:42 +


There are no notes attached to this issue.

-Issue History
Date Modified Username Field Change
2013-11-28 13:42 Jochen New Issue
2013-11-28 13:42 Jochen File Added: void.c
2013-11-28 13:47 yakobowski Status new => assigned
2013-11-28 13:47 yakobowski Assigned To => virgile
+Issue History