Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002170Frama-CKernel > ACSL implementationpublic2015-09-24 14:412015-09-24 14:41
Reporterpatrick 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0002170: ACSL typing fails when performing unification of type variables
DescriptionFrama-C fails while typing the given ACSL axiomatic.
Steps To Reproduce> cat list.i
//@ type List<A> = Nil | Cons(A,List<A>);

/*@ axiomatic L {
  @ predicate P(List l1, List l2);
  @ logic List<integer> aList{L} ;
  @ axiom a: P(Nil, aList);
  @ }
  @*/
> frama-c list.i
...
../tests/list.i:8:[kernel] user error: invalid implicit conversion from ℤ to A#4
Additional InformationTyping is succesful when axiom "a" is replaced by:
   @ axiom a: P(aList,Nil);
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2015-09-24 14:41 patrick New Issue
2015-09-24 14:41 patrick Status new => assigned
2015-09-24 14:41 patrick Assigned To => virgile


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker