Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001838Frama-CPlug-in > E-ACSLpublic2014-07-16 18:152014-09-15 17:35
Reporterarvidj 
Assigned Toguillaume-petiot 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFrama-C Neon-20140301Fixed in Version 
Summary0001838: User defined function with specification memset conflicts with __e_acsl_memset in e_acsl_mmodel.c
DescriptionIf the user defines a function "memset" with specifications, then the generated function will be called __e_acsl_memset. But there is already such a function in e_acsl_mmodel.c, so there is an error on linking. Example: /*@ requires \valid(p) ; */ int memset(char *p) { return 123; } int main() { char *s = "toto"; memset(s); return 0; } When compiling and linking: /tmp/ccRT0UnW.o: In function `__e_acsl_memset': scratch.gen.c:(.text+0x14): multiple definition of `__e_acsl_memset' /tmp/cc8qdTOL.o:e_acsl_mmodel.c:(.text+0x2b): first defined here collect2: error: ld returned 1 exit status
TagsNo tags attached.
Attached Filesc file icon bug-memset.c [^] (128 bytes) 2014-07-16 18:15 [Show Content]

- Relationships

-  Notes
(0005465)
signoles (manager)
2014-09-15 17:35

Fixed in E-ACSL 0.4.1.

- Issue History
Date Modified Username Field Change
2014-07-16 18:15 arvidj New Issue
2014-07-16 18:15 arvidj Status new => assigned
2014-07-16 18:15 arvidj Assigned To => signoles
2014-07-16 18:15 arvidj File Added: bug-memset.c
2014-07-16 18:53 signoles Status assigned => acknowledged
2014-08-05 14:01 signoles Assigned To signoles => guillaume-petiot
2014-08-05 14:01 signoles Status acknowledged => assigned
2014-08-05 14:13 signoles Status assigned => resolved
2014-08-05 14:13 signoles Resolution open => fixed
2014-09-15 17:35 signoles Note Added: 0005465
2014-09-15 17:35 signoles Status resolved => closed
2014-09-15 17:35 signoles Target Version => Frama-C Neon-20140301


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker