2021-03-03 03:45 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001831Frama-CPlug-in > E-ACSLpublic2014-09-15 17:20
Reporterarvidj 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001831: Command line arguments (argc/argv) are not marked as valid
DescriptionSee attached file for example. I have a fix coming for this.
TagsNo tags attached.
Attached Files
  • c file icon bug-main-args.c (120 bytes) 2014-07-11 10:28 -
    int main(int argc, char **argv) {
      /*@ assert \forall integer i; 0 <= i < argc ==> \valid(argv[i]) ; */
      return 0;
    }
    
    
    c file icon bug-main-args.c (120 bytes) 2014-07-11 10:28 +

-Relationships
related to 0001103assignedvirgile Default @requires property for the [main] function 
+Relationships

-Notes

~0005457

signoles (manager)

Fixed in E-ACSL v0.4.1.
+Notes

-Issue History
Date Modified Username Field Change
2014-07-11 10:28 arvidj New Issue
2014-07-11 10:28 arvidj Status new => assigned
2014-07-11 10:28 arvidj Assigned To => signoles
2014-07-11 10:28 arvidj File Added: bug-main-args.c
2014-07-11 12:27 yakobowski Relationship added related to 0001103
2014-07-11 12:49 signoles Status assigned => confirmed
2014-08-04 15:40 signoles Status confirmed => resolved
2014-08-04 15:40 signoles Resolution open => fixed
2014-09-15 17:20 signoles Fixed in Version => Frama-C Neon-20140301
2014-09-15 17:20 signoles Note Added: 0005457
2014-09-15 17:20 signoles Status resolved => closed
+Issue History