Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

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 
PlatformOSOS Version
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 Filesc file icon unused.c [^] (200 bytes) 2012-04-16 11:28 [Show Content]

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

-  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).

- 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

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker