2021-01-16 00:31 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000841Frama-CKernel > ACSL implementationpublic2011-10-10 14:14
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritytweakReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000841: no conversion int[] to int* for logic fct arg; exprs a and &a[0] treated differently
DescriptionIn the attached program, the logic function p expects an int* argument.

When supplied the int[] argument (a), the kernel reports a user error (line 8), which is at least unfamiliar to C programmers.

Supplying the argument (&a[0]) causes no error message (line 7).
TagsNo tags attached.
Attached Files
  • c file icon ftest.c (135 bytes) 2011-05-27 16:13 -
    //@ axiomatic ax { logic boolean p{L}(int *b); }
    
    int a[10];
    
    void ftest(void) {
        //@ assert p(&a[0]);
        //@ assert p( a   );
    }
    
    
    c file icon ftest.c (135 bytes) 2011-05-27 16:13 +

-Relationships
+Relationships

-Notes

~0001989

virgile (developer)

ACSL states specifically that a conversion from a C array to a pointer must be done explicitly (either through a cast or by taking the address of the first element). I'll change the error message to a more specific one in this case.
+Notes

-Issue History
Date Modified Username Field Change
2011-05-27 16:13 Jochen New Issue
2011-05-27 16:13 Jochen File Added: ftest.c
2011-05-27 16:50 signoles Status new => assigned
2011-05-27 16:50 signoles Assigned To => virgile
2011-05-27 16:50 signoles Category Kernel => Kernel > ACSL implementation
2011-06-15 20:07 monate Status assigned => acknowledged
2011-06-22 13:47 virgile Note Added: 0001989
2011-06-22 14:12 svn
2011-06-22 14:12 svn Status acknowledged => resolved
2011-06-22 14:12 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
+Issue History