2021-03-02 03:10 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001162Frama-CKernel > ACSL implementationpublic2012-09-19 17:16
Reporternmuller 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001162: "for" clause is refused
DescriptionThe following annotation is refused :
    ensures \result == {s for a = (int)4 };

in the file StructTestPos.c
Additional Information[kernel] preprocessing with "gcc -C -E -I. -dD StructTestPos.c"
StructTestPos.c:38:[kernel] user error: unexpected token 'for'
[kernel] user error: skipping file "StructTestPos.c" that has errors.
[kernel] Frama-C aborted because of invalid user input.
TagsNo tags attached.
Attached Files
  • c file icon StructTestPos.c (624 bytes) 2012-04-16 18:26 -
    struct s {int a;}; 
    
    //@ ensures \result == 4;
    int field_eq_load(void)
    {
      struct s s1,s2; 
      s1.a =4; 
      s2 = s1; 
      return s2.a;
    }
    
    struct s s1,s2;
    //*@ ensures  s2 == s1; 
    void equal_record_test(void)
    {
      s2 =s1 ; 
      
    }
    
    struct Ts {struct s s1; int t[10];} ; 
    
    struct Ts ts1, ts2; 
    //@ ensures \result == ts1.t[0] ;
    int equal_with_array_field (void)
    {
      ts1=ts2; 
      return ts2.t[0];
    }
    
    struct S {int a;}; 
    
    struct S s;
    
    
    /*@ requires s.a == 5; 
        assigns s.a; 
        ensures \result == s;
        ensures \result == {s for a = (int)4 }; 
    */
    struct S ret_struct(void)
    {
      s.a = 4;
      return s;
    }
    int main (void) { return 0 ; }
    
    c file icon StructTestPos.c (624 bytes) 2012-04-16 18:26 +

-Relationships
+Relationships

-Notes

~0002932

virgile (developer)

Correct syntax for functional update is { s \with .a = 4 } (see ACSL manual at http://frama-c.com/download/acsl_1.5.pdf). It is supported by Frama-C's kernel in Nitrogen (although the implementation manual does not reflect it). Not all plug-ins have support for it, though.
+Notes

-Issue History
Date Modified Username Field Change
2012-04-16 18:26 nmuller New Issue
2012-04-16 18:26 nmuller Status new => assigned
2012-04-16 18:26 nmuller Assigned To => virgile
2012-04-16 18:26 nmuller File Added: StructTestPos.c
2012-04-17 17:41 virgile Note Added: 0002932
2012-04-17 17:41 virgile Status assigned => resolved
2012-04-17 17:41 virgile Fixed in Version => Frama-C Nitrogen-20111001
2012-04-17 17:41 virgile Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version Frama-C Nitrogen-20111001 => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
+Issue History