2021-01-27 08:20 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001154Frama-CPlug-in > jessiepublic2012-04-16 11:282012-04-17 17:31
Reporternmuller 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0001154: erroneous left value (structure field)
Descriptionaccess to a structure field in a lemna does not seem to work

typedef struct { int i; } T;

/*@ lemma toto{L}:
  @ \forall T t; t.i == 0;
  @*/
Additional Information frama-c -jessie -jessie-atp alt-ergo unused.c
[kernel] preprocessing with "gcc -C -E -I. -dD unused.c"
[jessie] Starting Jessie translation
unused.c:4:[jessie] failure: cannot handle this lvalue
[jessie] warning: Unsupported feature(s).
                  Jessie plugin can not be used on your code.


rem : as soon as t is actually declared (of type T) prior to the lemna and an explicit access to t.i is done, this works
TagsNo tags attached.
Attached Files
  • c file icon unused.c (200 bytes) 2012-04-16 11:28 - 
    typedef struct { int i; } T;

T t;

/*@ lemma toto{L}:
  @ \forall T t; t.i == 0;
  @*/


extern int G;

/*@ global invariant G_const: G == 0; */

static int i;

/*@ global invariant invi: i >= 0; */
    c file icon unused.c (200 bytes) 2012-04-16 11:28 +

-Relationships
duplicate of 0001156closedcmarche struct type not supported in type invariant 
+Relationships

-Notes

~0002885

nmuller (reporter)

2012-04-16 16:49

 yes sure, I would have expected of course that t.i == 0 works, provided that we declare T t; in front of the lemna...

~0002897

nmuller (reporter)

2012-04-16 18:56

 Under Nitrogen :
frama-c -jessie file.c -> KO
frama-c -jessie -jessie-atp file.c -> KO

~0002915

nmuller (reporter)

2012-04-17 13:47

 it seems to work with wp on the gui

~0002925

virgile (developer)

2012-04-17 15:58

 It seems like Jessie is not able to handle t.i when t is a logic variable (probably because it cannot transform it into &t->i like for a C lval).
+Notes

-Issue History
Date Modified Username Field Change
2012-04-16 11:28 nmuller New Issue
2012-04-16 11:28 nmuller Status new => assigned
2012-04-16 11:28 nmuller Assigned To => virgile
2012-04-16 11:28 nmuller File Added: unused.c
2012-04-16 12:44 yakobowski Relationship added duplicate of 0001159
2012-04-16 16:49 nmuller Note Added: 0002885
2012-04-16 18:56 nmuller Note Added: 0002897
2012-04-17 13:47 nmuller Note Added: 0002915
2012-04-17 15:58 virgile Note Added: 0002925
2012-04-17 15:58 virgile Assigned To virgile => cmarche
2012-04-17 15:58 virgile Category Kernel > ACSL implementation => Plug-in > jessie
2012-04-17 15:58 virgile Product Version Frama-C Carbon-20110201 => Frama-C GIT, precise the release id
2012-04-17 17:31 virgile Relationship added duplicate of 0001156
2012-04-17 17:43 virgile Relationship deleted 0001159
+Issue History