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 = Nil | Cons(A,List); /*@ axiomatic L { @ predicate P(List l1, List l2); @ logic List 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